セミナーの内容

参加者が自分の好きなプログラミング言語でデッドロック発見器を作り，それを使ってマルチスレッドプログラミングを学ぶハンズオンセミナーです．

作っていただくデッドロック発見器はマルチスレッドプログラムの動き全体を状態遷移図として可視化し，その過程でデッドロック状態を発見するというものです．以下にデッドロック発見器の出力例を示しました．

水色の状態は初期状態で，赤い状態がデッドロック状態です．デッドロック状態からは遷移が1つも出ていないので，この状態に達するとプログラムは停止してしまうことがわかります．動作し続けるパスもあり，必ず再現するわけではないというマルチスレッドプログラムに特徴的な問題であることが見てとれます．

セミナーのゴールは，自分で作ったデッドロック発見器を問題に適用して，このような出力を得ることです．

デッドロックを発見するためにはマルチスレッドプログラムの動き全体を調べる必要があります．そのためには「マルチスレッドプログラムの動きとは何か？」ということを明確にする必要があります．プログラムで処理できるくらい明確にするということです．

「マルチスレッドプログラムの動きを明確にする」ということの中には「スレッド間の相互作用とは何かを明確にする」ということが含まれています．改めて考えてみると，スレッド間の相互作用とは何なのでしょうか？．共有変数やメッセージ通信といった数ある相互作用の中で「もっとも基礎的なものは何か」と考えてみると，ある1つの候補が見えてきます．それはイベント同期と呼ばれている仕組みです．

「イベント」も「同期」もよく耳にする言葉ですが，「イベント同期」が何を意味するかについては疑問に思われるでしょう．このセミナーではこのイベント同期という相互作用の仕組みを紹介し，それを通じてスレッド間の相互作用とは何かということを考えていきます．

驚くべきことに，イベント同期という仕組みを基本的な相互作用として採用すると，実世界で使われている共有変数やメッセージ通信といった多くの相互作用を説明することができます．別の言葉でいえばモデル化できるということです．したがって，イベント同期を基礎としてマルチスレッドプログラムの動きを明確にし，その上で動きを調べるプログラムを作ると，多くの相互作用について適用できるということです．

はじめは「こんな単純な仕組みで何ができるのか？」と思われるかもしれません．実世界で使い慣れた相互作用に関する知識が，新しい考え方を拒否するかもしれません．これは知的な挑戦です．考え方を飛躍させる必要があります．とても単純なものを基礎にするだけで，たくさんのことが説明できて性質を調べられるようになります．これはとても面白いことではないでしょうか．宇宙が素粒子と基本的な力で構成されているという話に似ています．

話を聞いているだけで、このような発想の転換ができるわけではありません．そこでこのセミナーでは，イベント同期の仕組みの実装と，それを使って様々な相互作用をモデル化する作業を，参加者自ら行っていただきます．それが理解に至るもっとも効果的な方法だと考えています．

理論を理解したり技術を習得したりしてきた経験を持つ人は皆知っていることだと思いますが，新しい考え方を身につけることは容易ではありません．しかし苦労して手に入れた後に見える風景は，山頂から見渡す風景のようなものです．足元だけを見て登り続けていたときには全貌が見えていなかったけれども，視界が開けて振り返った時，自分が登ってきた高さを知ります．そしてかつての自分が下に見える雲の中にいたことに気づくでしょう．ぜひセミナーに参加して，同じ風景を見てみませんか？

プログラム

A. マルチスレッドの理論的モデル

デッドロック発見器の基礎となる理論的モデルを解説します．

1. プログラムと状態遷移
2. イベント同期による相互作用
3. チャネルによるメッセージ通信
4. 並行合成

B. デッドロック発見器の設計と実装

はじめに OCaml と C による実装例を元にデッドロック発見器のしくみを解説します．それを参考に自分の発見器を設計・実装します．

1. イベントとプロセス（スレッド）の表現
2. 並行合成（グラフの生成と探索）
3. 可視化（状態遷移グラフ，デッドロックへのパス）

C. 応用：モデル化と検査・分析

いくつかの相互作用をイベント同期でモデル化してみます．さらに応用として，通信する2つのコンポーネント間のあるプロトコルについて，同期通信の場合と非同期通信の場合それぞれについて設計してみます．

1. バッファとキュー
2. 共有変数とミューテックス
3. 通信するコンポーネント間プロトコルの設計

D. 実装

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

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

講師について

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

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

国立情報学研究所トップエスイープロジェクト『モデル検査特論』講師．

セミナー参加の前提条件

前提知識

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

必要なもの

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

配布物 と Zoom URL

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

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

プログラムの規模

デッドロック発見器本体サンプル実装の規模は次のとおりです．

• OCaml 197行
• C言語 377行（他にハッシュ表 94行，キュー 66行，ヘッダファイルを含む，合計 537行）

しくみを明らかにするために，エラー処理やメモリ解放などは意図的に省略しています．

調べる対象となるマルチスレッドプログラムは，状態遷移モデルとして表現します．このセミナー内ではモデル記述言語やパーサは作らないので，C言語の構造体初期化子または OCaml のデータ構造として手作業で記述します．例で扱うモデルは140行～200行程度です．

グラフ探索（幅優先探索または深さ優先探索）のプログラムを書くことになるので，すでに訪れたノードを記録するためにハッシュ表またはそれに類するデータ構造（辞書，マップなど）と，未調査のノードを格納しておくキューまたはスタックが必要です．OCaml 版では標準ライブラリの Hashtbl と Queue を使っています．C言語版では簡易な実装を用意しました．使用するプログラミング言語のライブラリに適切なものがない場合は自分で用意する必要があります．セミナーの時間は限られているので，本来の問題に集中するために事前に用意しておくとよいかもしれません．ノードはデッドロック発見器の利用者が定義する値を含むので，任意の型をキーとすることのできるハッシュ表が必要です．

注意事項

• 本セミナーで作成するデッドロック発見器は，抽象的な状態遷移表現を対象とするものです．特定のプログラミング言語で記述されたソースコードを対象するものではありません．また，すべての状態を調べるという性質上，適用できるプログラムの大きさに限界があります．
• 講師が知らないプログラミング言語については対処が限られます．
• 配布資料の公開は禁止です．

参考書

• ソフトウェア科学基礎

連絡先

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