セミナーの内容

第3回のテーマはデッドロックです．並行システムに特徴的なデッドロックはなぜ発生するのか，そのメカニズムを解説します．ツール SyncStitch にはデッドロックを検出する機能があります．その使い方を解説します．

第3回 プログラム

• 相互作用のモデル化2：共有メモリ（共有変数）
• ミューテックスによる排他制御
• デッドロック
• デッドロック検査

シリーズの構成

• 第1回 プロセスのモデル化
• 第2回 相互作用と並行合成
• 第3回 デッドロック
• 第4回 part 1: 内部遷移・隠蔽・非決定性・発散，part 2: 振る舞いとは何か
• 第5回 part 1: 正当性，part 2: トレース集合による安全性検査
• 第6回 安定失敗集合による正当性検査

講師について

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

CSP 理論に基づいたモデリング・検査ツール SyncStitch 開発者

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

セミナー参加の前提条件

前提知識

前提として必要な知識は，プログラミングの知識と状態遷移モデル（オートマトン）の知識です．マルチスレッド（プロセス・タスク）のプログラムを書いたことがあるという程度の知識を仮定します．排他制御といった概念やミューテックス，セマフォといった同期のための機構についての知識を仮定します．

一部，発展的な内容に関する部分では，高校で習う程度の集合の記法（要素 x ∈ A，部分集合 A ⊆ B など）を使います．

必要なもの

• PC（マウスが必要です）
• ツール SyncStitch https://github.com/hatsugai/SyncStitch/releases

Zoom URL

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

配布物

スライド資料（PDF)とモデルファイルを CONNPASS のメッセージにて配布します．

使用するツール

CSP 理論に基づいたモデリングと検査が可能な SyncStitch というツールを使用します．このツールで学んだ考え方と記法は他のツール（FDR, PAT, LTSA, ProB）でも活用できます（※これらのツール間でも細かい差異はあります）．

注意事項

• 配布スライド資料の公開は禁止です．
• 各回を2回ずつ開催します．都合の良い回を選んで参加してください．申し込み後に都合が悪くなってもう一方の回に参加したい場合，別の曜日の回には申し込まずにご連絡ください．もう一方の回に参加できるよう調整します．2重に申し込みをしても一方はキャンセルできません．

参考書

• 並行システムの検証と実装

連絡先

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