セミナーの内容

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

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

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

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

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

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

• 変数の値についての条件：（例）x = 0, x > 3，リストに指定要素が含まれている，など．
• 条件の結合： 否定（not），かつ（and），または（or）
• 次の状態で条件が成り立つような状態：（例）次の状態で変数 x が 0 になる．
• 実行パス上で常に条件が成り立つかどうか：（例）p と q が同時に 1 になることは決してない．
• 実行パス上でいつか条件が成り立つかどうか：（例）いつかは必ず off になる．

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

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

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

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

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

プログラム

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

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

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

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

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

C. 応用：検査と分析

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

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

講師について

株式会社PRINCIPIA 代表取締役 初谷 久史

プロセス代数 CSP に基づいた対話的モデリング・検査ツール SyncStitch 開発者．

国立情報学研究所トップエスイープロジェクト「並行システムの設計検証」講師．

セミナー参加の前提条件

前提知識

• マルチスレッドプログラミングについての基本的な知識：プロセス，スレッド，排他制御，ミューテックス，条件変数
• アルゴリズムの知識：グラフの探索（幅優先探索または深さ優先探索）
• データ構造の知識：ハッシュ表，キュー

必要なもの

• ノート PC
• 使用するプログラミング言語での開発環境（サンプル実装を動かすためには OCaml または C コンパイラが必要です）
• Graphviz （dot コマンド）：状態遷移グラフを可視化するために使用します．

配布物

セミナーの約1週間前にスライド資料（PDF)とサンプル実装のソースコード（C言語と OCaml）をメールにて送付します．

CONNPASS と PayPal に登録されているメールアドレスを今一度ご確認ください．

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

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

• OCaml 約200行
• C言語 約300行

注意事項

• このセミナーは「デッドロック発見器を作って学ぶマルチスレッドプログラミング ★共有変数編★」の続編です．「★メッセージ通信編★」の続編ではありません．
• 「デッドロック発見器を作って学ぶマルチスレッドプログラミング ★共有変数編★」に参加していない人でも参加できます．配布物にはデッドロック発見器のサンプル実装のソースコードも含まれています．（説明資料とサンプルモデルは含まれていません）．
• 講師が知らないプログラミング言語については対処が限られます．
• 配布資料の公開は禁止です．
• 録画・録音は禁止です．スチル写真撮影はかまいませんが，参加者が写る場合はご自分で許可を得てください．
• 飲食は可能ですが，ゴミはお持ち帰りください．
• 不測の事態によりセミナーが開催できなかった場合は，参加費用の返却にて対応させていただきます．
• CONNPASS ではなく PayPal に登録されているメールアドレスにご連絡を差し上げる場合があります．異なるメールアドレスを登録されている方はお見逃しがないようご注意ください．

参考書

• ソフトウェア科学基礎

参考：デッドロック発見器の実装例

「デッドロック発見器を作って学ぶマルチスレッドプログラミング ★共有変数編★」参加者で，実装を公開されている人がいらっしゃいます．

• https://github.com/Kuniwak/ddsv-prolog
• https://gist.github.com/ryohji/d2afd304dd6fb99e032897a8e1db5eb0
• https://github.com/y-taka-23/ddsv-go
• https://gist.github.com/hatsugai/49e68c2c9d952bc94684d7a7b83a62e7

連絡先

ご質問等がありましたら isaac@principia-m.com までお気軽にご連絡ください．