PRINCIPIA
Products Seminar About Us

トレース比較器を作って学ぶマルチスレッドプログラミング

「デッドロック発見器を作って学ぶマルチスレッドプログラミング ★メッセージ通信編★」の続編です．

デッドロック発見器ではイベント同期という単純なしくみを使って様々な相互作用が表現できることを見ました．相互作用を決めるとシステム全体の振る舞いも状態遷移という形で計算することができ，その過程でデッドロックを発見することができました．

イベントを基礎とした相互作用にはもう1つ優れている点があります．それはシステムの振る舞いを仕様と比較することによって設計の正しさを検証できるという点です．

システムの振る舞いは外部から観測可能なイベントを発生順に並べた列として表すことができます．これをトレースといいます．システムが発生しうるトレースがすべて仕様で許容されたものであれば，システムの振る舞いはかなりの精度で正しいということができます．

一般にシステムは停止せずに動作を継続しますから，いくらでも長いトレースがありえます．さらにシステムが生成しうるトレースの種類も無限になる可能性があります．そうすると有限のメモリしか持たない計算機で有限の時間内に仕様と実装のトレースを比較することは不可能であるように思えますが，興味深いことに模倣（simulation）という考え方を使うとこれが可能になります．この模倣を計算することによって仕様と実装のトレースを比較するプログラムがトレース比較器です．

このセミナーのゴールはトレース比較器を作って仕様とシステムの振る舞いを比較できるようになることです．

以下の例では，初期状態から緑色の遷移をたどって同じトレースがありますが，最後の赤い状態のところで，仕様にはないイベントをシステムが発生していることがわかります．

状態遷移図

トレースは外部から観測可能なイベントだけを含むようにします．ユーザが関心を持つのは外部から見える動作だけで，内部のつくりは関係ないからです．

しかしシステムはコンポーネントを組み合わせて作りますから，その間で行われる相互作用のためのイベントも含まれています．これは内部の都合であって，ユーザには関係しません．

そこでこのような内部で使われるイベントを外から見えなくする処理を行います．これを隠蔽といいます．システムに隠蔽処理をしてからトレース比較を行うということです．

プログラムの正しさを検証するツールの中には，仕様は仕様記述言語，実装はモデリング言語と，仕様・実装で異なる表現形式を使うものがあります．これに対してトレース比較器はどちらも状態遷移で表します．この対称性のおかげで面白いことができます．仕様と実装を交換して比較することです．もし双方向の比較に成功したら，この2つはまったく同じトレースを含んでいるということになります．つまりトレース比較器を使うと状態遷移の等価性を判定することができます．ただし，これには1つ条件があります．実装に非決定性という性質がないことです．これについては発展的な内容としてセミナー内で紹介します．

トレース比較器はシステムの全体の振る舞いだけでなく，要求段階で検討するようなシナリオなども比較することができます．仕様検討や設計の試行錯誤など，プログラム開発の初期段階を支援してくれる強力な武器になると思います．

プログラム

A. プログラムの正当性とトレース比較器のしくみ

  1. 正当性：プログラムが仕様を満たす条件
  2. トレースによる正当性の検査
  3. 模倣（simulation）
  4. トレース比較器のしくみ
  5. 内部動作と隠蔽
  6. 非決定性と決定化［発展］
  7. 振る舞いの等価性［発展］

B. トレース比較器の設計と実装

はじめに OCaml と C による実装例を元にトレース比較器の設計を解説します．それを参考に自分のトレース比較器を設計・実装します．

  1. 隠蔽
  2. トレース比較
  3. テスト
  4. 決定化［発展］

C. 応用：検査と分析

トレース比較器の典型的な使い方を紹介します．

  1. 排他制御の安全性検査
  2. バッファ結合とキューの等価性
  3. リーダ・ライタ問題

セミナー参加の前提条件

前提知識

必要なもの

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

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

参考書

© 2013-2023 PRINCIPIA Limited