PRINCIPIA
ProductsSeminarAbout Us

モデル検査器を作って学ぶマルチスレッドプログラミング

デッドロック発見器を作って学ぶマルチスレッドプログラミング ★共有変数編★」の続編です.

デッドロック発見器では各スレッドの振る舞いを状態遷移として記述し,それらを合成してシステム全体の状態遷移を計算しました.その過程で遷移のない状態,すなわちデッドロック状態を発見することができました.

システムの状態遷移全体が可視化できるようになると,デッドロック以外にもいろいろ気づく点があります.例えば想定していなかった遷移や分岐があるとか,変数の値がおかしな状態があるなどの点です.さらに状態遷移の流れを追って動作を確認したくなります.

状態遷移グラフが小さいうちは,画面上で追ったり,印刷をしてマークしながら確認したりすることができます.しかし実践的なモデルは状態数がとても多くなるので,グラフ上を目視で追うことは難しくなります.

そこでこのセミナーでは再びこの仕事を計算機にやってもらうという戦略をとります.データベースのクエリーのように,条件を指定してそれを満たす状態や実行パスを探すツールを作ります.このようなツールをモデル検査器といいます.

このセミナーで作っていただくモデル検査器では次のような条件を指定することができます:

セミナーのゴールは,自分で作成したデッドロック発見器を拡張し,条件を満たす状態に色を付けた,以下のような出力を得ることです.この例では3つのスレッドがロック獲得で競合しており,あるスレッドが要求しているにもかかわらずロックを獲得できない状態をマークしています.状態には成り立つ条件式も示しています.条件を様々に変えながらマークの付く状態を観察するのは実に楽しく,そうしているうちにシステムの振る舞いや性質がよくわかるようになります.

状態遷移図
状態遷移図

条件を表す式としては計算木論理(Compulation Tree Logic, CTL)というものを使います.世にあるモデル検査器でも使われている表現の1つで,プログラマにとっても親しみやすいものだと思います.計算木論理についてはセミナーの中で説明しますので予備知識は必要ありません.

計算木論理を学ぶとプログラムの実行について理解を深めることができます.システムが可能な実行パスという考え方を獲得できるからです.抽象的な条件式を形式的に知るだけでなく,実際に条件を満たす状態や実行パスを求めるプログラムを書いて使ってみると,それらがどういうものであるかということを深く理解することができます.

自らプログラムを書いた経験があれば,計算木論理をサポートした強力な既存のツールも習得しやすくなります.プログラムを書くことで背景のしくみを理解し,実際の応用では強力なツールを使うというのは効率的な習得の方法だと思います.

さらに,実行パスという考え方はテストで応用できる可能性があります.状態遷移上の実行パスからテストケースを作るというのが1つのアイデアです.もう1つは実システムを実行させたときのログを取り,これを状態遷移上の実行パスと比較するというアイデアです.状態遷移モデルを持っているとこのような可能性が広がります.

プログラム

A. 計算木論理(CTL)とモデル検査器のしくみ

  1. 計算木論理(CTL)
  2. モデル検査器のしくみ:マーキングアルゴリズム

B. モデル検査器の設計と実装

はじめに OCaml と C による実装例を元にモデル検査器の設計を解説します.それを参考に自分のモデル検査器を設計・実装します.

  1. 条件式の表現
  2. マーキングアルゴリズム
  3. モデル検査器のテスト

C. 応用:検査と分析

モデル検査器の典型的な使い方を紹介します.

  1. モデル検査器でデッドロックを発見する
  2. さまざまな条件による状態の探索
  3. 安全性の検査(おかしな状態が含まれていないこと)
  4. ライブネスの検査(いつか条件を満たす状態に至ること)

セミナー参加の前提条件

前提知識

必要なもの

プログラムの大きさの目安

モデル検査器のコード(デッドロック発見器に追加するコード)の大きさは,サンプル実装で次のとおりです.

参考書