読者です 読者をやめる 読者になる 読者になる

チェシャ猫の消滅定理

数学にプログラミング、素敵なもの何もかも。

NGK2014B で SPIN について話してきました

名古屋工業大学で行われた LT 大会 NGK2014B で発表しました。

内容はタイトルそのままで、モデル検査ツール SPIN とその記述言語である Promela の特徴を概観する、というものです。

当日の動画は Youtube から見ることができます。

ちなみに、発表順は乱数で決められているはずなのですが、なぜか去年の NGK と全く同じ 3 番目でした。

リソース共有問題の Promela モデル

LT の冒頭に登場するリソース共有時のデッドロックについて、Promela で記述したモデルが Gist においてあります。

この Promela モデルは、次のようなシステムを想定したものです。

  • クライアント
    1. スキャナもしくはプリンタのどちらかをロックし、その後もう片方をロック
    2. スキャナもしくはプリンタのどちらかをアンロックし、その後もう片方をアンロック
  • リソース (スキャナ、プリンタ)
    1. ロックするメッセージを待ち、相手のプロセス ID を記憶
    2. アンロックするメッセージを待ち、相手のプロセス ID とロックしたプロセスを照合
    3. ロックとアンロックが同じプロセスからのものならば最初に戻る

すぐわかる通り (LT 内でも述べていますが) このシステムには欠陥があり、デッドロックが発生します。スキャナとプリンタにロックを掛ける順番が指定されていない (そして Promela がそういう非決定的な記述を許す) というところがポイントです。

いずれこのモデルを題材にして Promela/SPIN の入門記事でも書くつもりではありますが、それはまた別の話。