モデル検査器を作って学ぶマルチスレッドプログラミング
「デッドロック発見器を作って学ぶマルチスレッドプログラミング ★共有変数編★」の続編です．
デッドロック発見器では各スレッドの振る舞いを状態遷移として記述し，それらを合成してシステム全体の状態遷移を計算しました．その過程で遷移のない状態，すなわちデッドロック状態を発見することができました．
システムの状態遷移全体が可視化できるようになると，デッドロック以外にもいろいろ気づく点があります．例えば想定していなかった遷移や分岐があるとか，変数の値がおかしな状態があるなどの点です．さらに状態遷移の流れを追って動作を確認したくなります．
状態遷移グラフが小さいうちは，画面上で追ったり，印刷をしてマークしながら確認したりすることができます．しかし実践的なモデルは状態数がとても多くなるので，グラフ上を目視で追うことは難しくなります．
そこでこのセミナーでは再びこの仕事を計算機にやってもらうという戦略をとります．データベースのクエリーのように，条件を指定してそれを満たす状態や実行パスを探すツールを作ります．このようなツールをモデル検査器といいます．
このセミナーで作っていただくモデル検査器では次のような条件を指定することができます：
- 変数の値についての条件：（例）x = 0, x > 3，リストに指定要素が含まれている，など．
- 条件の結合： 否定（not），かつ（and），または（or）
- 次の状態で条件が成り立つような状態：（例）次の状態で変数 x が 0 になる．
- 実行パス上で常に条件が成り立つかどうか：（例）p と q が同時に 1 になることは決してない．
- 実行パス上でいつか条件が成り立つかどうか：（例）いつかは必ず off になる．
セミナーのゴールは，自分で作成したデッドロック発見器を拡張し，条件を満たす状態に色を付けた，以下のような出力を得ることです．この例では3つのスレッドがロック獲得で競合しており，あるスレッドが要求しているにもかかわらずロックを獲得できない状態をマークしています．状態には成り立つ条件式も示しています．条件を様々に変えながらマークの付く状態を観察するのは実に楽しく，そうしているうちにシステムの振る舞いや性質がよくわかるようになります．
条件を表す式としては計算木論理（Compulation Tree Logic, CTL）というものを使います．世にあるモデル検査器でも使われている表現の1つで，プログラマにとっても親しみやすいものだと思います．計算木論理についてはセミナーの中で説明しますので予備知識は必要ありません．
計算木論理を学ぶとプログラムの実行について理解を深めることができます．システムが可能な実行パスという考え方を獲得できるからです．抽象的な条件式を形式的に知るだけでなく，実際に条件を満たす状態や実行パスを求めるプログラムを書いて使ってみると，それらがどういうものであるかということを深く理解することができます．
自らプログラムを書いた経験があれば，計算木論理をサポートした強力な既存のツールも習得しやすくなります．プログラムを書くことで背景のしくみを理解し，実際の応用では強力なツールを使うというのは効率的な習得の方法だと思います．
さらに，実行パスという考え方はテストで応用できる可能性があります．状態遷移上の実行パスからテストケースを作るというのが1つのアイデアです．もう1つは実システムを実行させたときのログを取り，これを状態遷移上の実行パスと比較するというアイデアです．状態遷移モデルを持っているとこのような可能性が広がります．
プログラム
A. 計算木論理（CTL）とモデル検査器のしくみ
- 計算木論理（CTL）
- モデル検査器のしくみ：マーキングアルゴリズム
B. モデル検査器の設計と実装
はじめに OCaml と C による実装例を元にモデル検査器の設計を解説します．それを参考に自分のモデル検査器を設計・実装します．
- 条件式の表現
- マーキングアルゴリズム
- モデル検査器のテスト
C. 応用：検査と分析
モデル検査器の典型的な使い方を紹介します．
- モデル検査器でデッドロックを発見する
- さまざまな条件による状態の探索
- 安全性の検査（おかしな状態が含まれていないこと）
- ライブネスの検査（いつか条件を満たす状態に至ること）
セミナー参加の前提条件
前提知識
- マルチスレッドプログラミングについての基本的な知識：プロセス，スレッド，排他制御，ミューテックス，条件変数
- アルゴリズムの知識：グラフの探索（幅優先探索または深さ優先探索）
- データ構造の知識：ハッシュ表，キュー
必要なもの
- ノート PC
- 使用するプログラミング言語での開発環境（サンプル実装を動かすためには OCaml または C コンパイラが必要です）
- Graphviz （dot コマンド）：状態遷移グラフを可視化するために使用します．
プログラムの大きさの目安
モデル検査器のコード（デッドロック発見器に追加するコード）の大きさは，サンプル実装で次のとおりです．
- OCaml 約200行
- C言語 約300行