セミナーの内容

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

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

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

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

マルチスレッドプログラミングの教科書を見ると，典型的なアルゴリズムが解説されています．それが自分のプログラムでそのまま使える場合はよいのですが，そうではない場合は一部を変更したり新しいアルゴリズムを考案したりすることになります．ところがマルチスレッドプログラミングというのは難しいもので，少し修正しただけで動かなくなったり，一見うまく動いているように見えても長時間動かしていると時々おかしくなる，というようなことが起こったりします．このようなときはどうしたらよいのでしょうか．

こういうときに役に立つのは基礎的な理論の力です．プログラムの動きとは何か，それらを複数並行に走らせるマルチスレッドプログラムの動きとは何か，といった基本的なことがらを明確にすると，プログラムの動きをデータとして表現することができます．プログラムの動きがデータになればプログラムで操作ができます．すると計算機のパワーを使ってプログラムの動きを調べ尽くし，おかしなところがないかどうかチェックすることができます．つまり理論の力を借りてプログラムの動きを調べるプログラムを作ることで問題に対処しようというわけです．

実はそのような方針で作られたツールはたくさんあります．しかし使いこなすためには基礎となる理論を学ぶ必要があり，やや敷居が高く感じる人が多いようです．理論が難しいということもありますが，抽象的な理論はなかなか頭に染み込まず，実際の問題との関係が見えにくいという感想をよく聞きます．

そこでこのセミナーでは，理論の中でももっとも基礎的で簡単な部分だけを使い，プログラムの動きを調べるプログラムを自ら作るというアプローチを採用します．理論を理解するもっともよい方法は，実際に使ってみることです．プログラミングの場合でいえばプログラムを書いてみることです．教科書を読んだだけではわかったつもり，本当に理解できたと思えるのはあれこれ調査・試行錯誤してプログラムを書いたときであることは誰もが経験的に感じていることでしょう．自分のものにするというのは，教科書に書いてあることを自分で再現・応用できるようになるということだと思います．

このセミナーにはもう1つ特徴があります．解決すべき問題に集中するためには慣れた道具を使う方がよいでしょう．そこで使用するプログラミング言語は参加者が自由に選ぶ，というスタイルにしました．サンプル実装は C 言語版と OCaml 版の2つを用意してあります．参加者は自分のペースで作業を進めることができます．たとえば次のような方針があります：

• 理論の解説を聞いたら，あとは自分で設計・実装する
• サンプル実装を読み解いて，自分の好きな言語で実装する
• サンプル実装の解説を参考に，自分の好きな言語で実装する
• サンプル実装を動かしたり，コードを読んだり，改造したりして理解を深める

サンプル実装は疑似コードではなく実際に動くプログラムなので，実装する自信はないけれども動かしたりコードを読んで質問したりして理解したいという人でも参加できます．一方，余力のある人向けには発展課題も用意してあります．

デッドロック発見器ができたら次は応用です．実際のマルチスレッドプログラムに適用してみます．基本的な3つの例を用意しました．サンプル実装でも参加できます．余力のある人は自分が興味のあるプログラムに適用してみてください．わかる範囲で質問もお受けします．

上に示した状態遷移図の例からもわかるように，デッドロック発見器が教えてくれるのはデッドロックがある・ないということと，ある場合にはその状態と初期状態からの実行パスです．しかし「なぜデッドロックするのか？」という問いには答えてくれません．実行パスを読み解いてデッドロックする理由（設計やアルゴリズムの間違い）を理解するのは人間の仕事です（いまのところ）．実は，この実行パスを読み解くという作業がマルチスレッドプログラミングの力をつけてくれるとても有効なトレーニングになります．デッドロック発見器はプログラマがコーディング時に想定していなかった組み合わせのパスを確実に見つけてくるからです．この読み解き作業を数多くこなしていくと，想定できる範囲が広がり，危ないコーディングに気づけるようになります．正しいフィードバックと深い思考を数多く経験することによって直感が働くように脳を鍛えるということだと思います．

プログラミングの分野では次々と新しい技術が登場し，急激に変化を続けていますが，一方で基礎的な理論の価値はそうそう変わらないものです．一度身に着ければ一生役に立つ理論を，自ら手を動かし，講師と対話することで深く効率よく習得できるこのセミナーにぜひご参加ください．自分で作ったツールというのは愛着のわくものです．作って楽しく，使って役に立ち，継続的に育てる楽しみもあります．

プログラム

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

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

1. プログラムと状態遷移
2. 相互作用（共有変数とメッセージパッシング）

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

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

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

C. 応用：同期オブジェクトのモデル化と検査・分析

作ったデッドロック発見器を使って，マルチスレッドプログラムの設計問題を扱ってみます．

1. ミューテックスによる排他制御
2. キューによる非同期通信
3. 条件変数によるキューの実装

D. 実装

各自、デッドロック発見器を好きな言語で設計・実装します。

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

講師について

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

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

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

セミナー参加の前提条件

前提知識

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

必要なもの

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

Zoom URL

CONNPASS のメッセージにてお知らせします。

配布物

スライド資料（PDF)とサンプル実装のソースコード（C言語と OCaml）を CONNPASS のメッセージにて配布します．

プログラムの規模

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

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

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

C言語版の方が少し機能が多くなっています：

• 初期状態からデッドロック状態へ至るパスの色付け
• 遷移における実行スレッド名の表示
• 可視化部での状態の整列（Graphviz の出力が少し見やすくなるため）

同様の拡張を OCaml 版に対して行うことはそれほど難しくないのですが，OCaml 版はリファレンスとしてシンプルさを保ちたいのでこのような形になっています．

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

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

注意事項

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

参考書

• ソフトウェア科学基礎

事例

デッドロック発見器を使った事例や，前回のセミナーに参加された人の作品を紹介しています．

• https://twitter.com/iriyak/status/1185572136838029312
• https://twitter.com/iriyak/status/1185753224390696960
• https://twitter.com/iriyak/status/1185827391672737792
• https://twitter.com/iriyak/status/1185919285828313089
• https://github.com/Kuniwak/ddsv-prolog
• https://gist.github.com/ryohji/d2afd304dd6fb99e032897a8e1db5eb0
• https://twitter.com/elkel53930/status/1186229966461124609
• https://twitter.com/elkel53930/status/1186250611718676480
• https://twitter.com/ikb/status/1185963135317897217
• https://twitter.com/ikb/status/1186339181712166912
• https://twitter.com/ikb/status/1186343402289262594
• https://twitter.com/ikb/status/1187043525256331264
• https://twitter.com/ikb/status/1187043533233872897
• https://twitter.com/ikb/status/1187045534273425408
• https://twitter.com/ikb/status/1191363692224339970
• https://gist.github.com/hatsugai/49e68c2c9d952bc94684d7a7b83a62e7
• https://github.com/y-taka-23/ddsv-go

続編について

このセミナーには続編があります．続編ではデッドロック発見器をモデル検査器にバージョンアップします．

連絡先

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