セミナーの内容

「トレース比較器を作って学ぶマルチスレッドプログラミング」の続編です．

トレース比較器では模倣という考え方を使って仕様と実装のモデルを比較することができました．テストとは異なり，実装が持つすべての振る舞いを網羅的に検査できるというところがポイントでした．

トレースによる仕様と実装モデルの比較では安全性が検査できました．実装モデルが仕様で規定されている範囲の外に悪い動作を決して行わないということが検査できました．

その一方でトレース比較器には2つの欠点がありました：

1. 仕様が発生を要求するイベントが必ず発生すること（ライブネス）を確認できない．
2. 非決定性を区別できない．

このセミナーでは上記2つの欠点を解決したより完全な仕様と実装モデルの比較器「リファインメント検査器」を作ります．

リファインメントとは何か

一般にプログラムを開発する過程では，仕様からはじめて設計の詳細を段階的に詰めていき最後にコードにします．正しくできた実装コードと仕様との間には正当性関係が成り立つといいますが，設計の中間段階の表現もある意味仕様を満たしているはずです．そこでこの正当性という関係の対象を仕様と実装だけに限らず設計の中間成果物に拡大してリファインメント関係（詳細化関係）といいます．仕様とある設計表現や，設計表現Aと設計表現Bの間にリファインメント関係が成り立つとか成り立たないとかいうわけです．

トレース比較器はリファインメント検査器の1種です．その基準であるトレース集合の包含関係は安全性を検査するには十分ですが，ライブネスと非決定性まで含めて検査するには精度が足りませんでした．

そこでこのセミナーではライブネスと非決定性を識別するために拒否という概念を導入し，より精度の高いリファインメント検査器を作ります．

リファインメント検査器を使うと十分な精度で仕様と実装モデルが比較できます．まずトレース比較器ではできなかった「イベントが必ず発生する」というライブネスの要求を表現し検査できます．加えて非決定性に関する振る舞いを検査できる点が大きなポイントです．非決定性はいわゆる再現性の難しいバグやタイミングで発生したりしなかったりするバグの原因となるものです．原理上，これらの問題が解決したことをテストで保証することはできません．しかし非決定性を識別する能力のあるリファインメント検査器では問題がないことを確実に確認することができます．以上の点からリファインメント検査器は強力な設計支援のツールとなるでしょう．

プログラム

A. リファインメント

1. トレース集合は非決定性を識別できない
2. 拒否：非決定性の表現
3. 安定失敗
4. リファインメント：リアクティブシステムの正当性条件
5. リファインメント検査アルゴリズム
6. 極大拒否・極小受理

B. リファインメント検査器の設計と実装

OCaml と C による実装例を元にリファインメント検査器の設計を解説します．

1. 極小受理と極小受理集合の表現
2. リファインメント検査
3. テスト

C. 適用事例

• 生産者・消費者問題（セマフォ解）

D. 実装

各自、好きな言語で設計・実装します．

※ セミナー時間内に完成させることは想定していません．セミナー後各自実装していただくことを想定しています．質問はメールまたは Slack にて受け付けます．

講師について

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

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

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

セミナー参加の前提条件

前提知識

• マルチスレッドプログラミングについての基本的な知識：プロセス，スレッド，排他制御，ミューテックス，条件変数
• データ構造の知識：集合の操作

必要なもの

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

配布物と Zoom URL

申し込み締め切り時刻後に CONNPASS のメッセージにてお知らせします．

事前に何度か配布する場合があります．同じ何度もメッセージが複数回届きますがご了承ください．

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

リファインメント検査器のコード（トレース比較器に追加するコード）の大きさは，サンプル実装で次のとおりです．

• OCaml 約210行
• C言語 約230行

注意事項

• このセミナーは「トレース比較器作って学ぶマルチスレッドプログラミング」の続編です．
• 講師が知らないプログラミング言語については対処が限られます．
• 配布資料の公開は禁止です．

参考書

• ソフトウェア科学基礎
• 並行システムの検証と実装

連絡先

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