トレース比較器を作って学ぶマルチスレッドプログラミング
セミナーの内容
「デッドロック発見器を作って学ぶマルチスレッドプログラミング ★メッセージ通信編★」の続編です．
デッドロック発見器ではイベント同期という単純なしくみを使って様々な相互作用が表現できることを見ました．相互作用を決めるとシステム全体の振る舞いも状態遷移という形で計算することができ，その過程でデッドロックを発見することができました．
イベントを基礎とした相互作用にはもう1つ優れている点があります．それはシステムの振る舞いを仕様と比較することによって設計の正しさを検証できるという点です．
システムの振る舞いは外部から観測可能なイベントを発生順に並べた列として表すことができます．これをトレースといいます．システムが発生しうるトレースがすべて仕様で許容されたものであれば，システムの振る舞いはかなりの精度で正しいということができます．
一般にシステムは停止せずに動作を継続しますから，いくらでも長いトレースがありえます．さらにシステムが生成しうるトレースの種類も無限になる可能性があります．そうすると有限のメモリしか持たない計算機で有限の時間内に仕様と実装のトレースを比較することは不可能であるように思えますが，興味深いことに模倣（simulation）という考え方を使うとこれが可能になります．この模倣を計算することによって仕様と実装のトレースを比較するプログラムがトレース比較器です．
このセミナーのゴールはトレース比較器を作って仕様とシステムの振る舞いを比較できるようになることです．
以下の例では，初期状態から緑色の遷移をたどって同じトレースがありますが，最後の赤い状態のところで，仕様にはないイベントをシステムが発生していることがわかります．
トレースは外部から観測可能なイベントだけを含むようにします．ユーザが関心を持つのは外部から見える動作だけで，内部のつくりは関係ないからです．
しかしシステムはコンポーネントを組み合わせて作りますから，その間で行われる相互作用のためのイベントも含まれています．これは内部の都合であって，ユーザには関係しません．
そこでこのような内部で使われるイベントを外から見えなくする処理を行います．これを隠蔽といいます．システムに隠蔽処理をしてからトレース比較を行うということです．
プログラムの正しさを検証するツールの中には，仕様は仕様記述言語，実装はモデリング言語と，仕様・実装で異なる表現形式を使うものがあります．これに対してトレース比較器はどちらも状態遷移で表します．この対称性のおかげで面白いことができます．仕様と実装を交換して比較することです．もし双方向の比較に成功したら，この2つはまったく同じトレースを含んでいるということになります．つまりトレース比較器を使うと状態遷移の等価性を判定することができます．ただし，これには1つ条件があります．実装に非決定性という性質がないことです．これについては発展的な内容としてセミナー内で紹介します．
トレース比較器はシステムの全体の振る舞いだけでなく，要求段階で検討するようなシナリオなども比較することができます．仕様検討や設計の試行錯誤など，プログラム開発の初期段階を支援してくれる強力な武器になると思います．
プログラム
A. プログラムの正当性とトレース比較器のしくみ
- 正当性：プログラムが仕様を満たす条件
- トレースによる正当性の検査
- 模倣（simulation）
- トレース比較器のしくみ
- 内部動作と隠蔽
- 非決定性と決定化［発展］
- 振る舞いの等価性［発展］
B. トレース比較器の設計と実装
OCaml と C による実装例を元にトレース比較器の設計を解説します．
- 隠蔽
- トレース比較
- テスト
- 決定化［発展］
C. 応用：検査と分析
トレース比較器の典型的な使い方を紹介します．
- 排他制御の安全性検査
- バッファ結合とキューの等価性
- リーダ・ライタ問題
D. トレース比較器の実装
各自、トレース比較器を好きな言語で設計・実装します。
※ セミナー時間内に完成させることは想定していません。セミナー後各自実装していただくことを想定しています。質問はメールにて受け付けます。
講師について
株式会社PRINCIPIA 代表取締役 初谷 久史
プロセス代数 CSP に基づいた対話的モデリング・検査ツール SyncStitch 開発者．
国立情報学研究所トップエスイープロジェクト「並行システムの設計検証」講師．
セミナー参加の前提条件
前提知識
- マルチスレッドプログラミングについての基本的な知識：プロセス，スレッド，排他制御，ミューテックス，条件変数
- アルゴリズムの知識：グラフの探索（幅優先探索または深さ優先探索）
- データ構造の知識：ハッシュ表，キュー
必要なもの
- 使用するプログラミング言語での開発環境（サンプル実装を動かすためには OCaml または C コンパイラが必要です）
- Graphviz （dot コマンド）：状態遷移グラフを可視化するために使用します．
配布物と Zoom URL
申し込み締め切り時刻後に CONNPASS のメッセージにてお知らせします。
事前に何度か配布する場合があります．同じ何度もメッセージが複数回届きますがご了承ください
プログラムの大きさの目安
トレース比較器のコード（デッドロック発見器に追加するコード）の大きさは，サンプル実装で次のとおりです．
- OCaml 約100行（＋決定化 約60行）
- C言語 約150行（＋決定化 約100行＋整数の集合ライブラリ 約100行）
注意事項
- このセミナーは「デッドロック発見器を作って学ぶマルチスレッドプログラミング ★メッセージ通信編★」の続編です．「★共有変数編★」の続編ではありません．
- 講師が知らないプログラミング言語については対処が限られます．
- 配布資料の公開は禁止です．
参考書
連絡先
ご質問等がありましたら isaac@principia-m.com までお気軽にご連絡ください．