NGK2014B で SPIN について話してきました
名古屋工業大学で行われた LT 大会 NGK2014B で発表しました。
内容はタイトルそのままで、モデル検査ツール SPIN とその記述言語である Promela の特徴を概観する、というものです。
当日の動画は Youtube から見ることができます。
ちなみに、発表順は乱数で決められているはずなのですが、なぜか去年の NGK と全く同じ 3 番目でした。
リソース共有問題の Promela モデル
LT の冒頭に登場するリソース共有時のデッドロックについて、Promela で記述したモデルが Gist においてあります。
この Promela モデルは、次のようなシステムを想定したものです。
- クライアント
- スキャナもしくはプリンタのどちらかをロックし、その後もう片方をロック
- スキャナもしくはプリンタのどちらかをアンロックし、その後もう片方をアンロック
- リソース (スキャナ、プリンタ)
- ロックするメッセージを待ち、相手のプロセス ID を記憶
- アンロックするメッセージを待ち、相手のプロセス ID とロックしたプロセスを照合
- ロックとアンロックが同じプロセスからのものならば最初に戻る
すぐわかる通り (LT 内でも述べていますが) このシステムには欠陥があり、デッドロックが発生します。スキャナとプリンタにロックを掛ける順番が指定されていない (そして Promela がそういう非決定的な記述を許す) というところがポイントです。
いずれこのモデルを題材にして Promela/SPIN の入門記事でも書くつもりではありますが、それはまた別の話。
