並行システムの設計検証 第2回 デッドロック・ライブロック
イベント内容
※ connpass からお申し込みができない場合、isaac@principia-m.com までご連絡ください。
セミナーの内容
第2回は「デッドロック・ライブロック」です.並行システムに典型的な2つの問題であるデッドロックとライブロックが発生するメカニズムを解説し,これらを検査によって発見する方法を解説します.
セミナーシリーズ全体についての説明は第1回のページをご覧ください.
プログラム
デッドロック
- 相互作用のモデル化2:共有メモリ(共有変数)
- ミューテックスによる排他制御
- デッドロック
- デッドロック検査
内部遷移・隠蔽・非決定性・発散
- 内部イベントと内部遷移
- 隠蔽
- 非決定性
- 発散(ライブロック)
- 発散検査
シリーズの構成
- 第1回 プロセスと相互作用
- 第2回 デッドロック・ライブロック
- 第3回 安全性検査
- 第4回 正当性検査
講師について
株式会社 PRINCIPIA 代表取締役 初谷 久史
CSP 理論に基づいたモデリング・検査ツール SyncStitch 開発者
国立情報学研究所トップエスイープロジェクト「並行システムの設計検証」講師
セミナー参加の前提条件
前提知識
前提として必要な知識は、プログラミングの知識と状態遷移モデル(オートマトン)の知識です。マルチスレッド(プロセス・タスク)のプログラムを書いたことがあるという程度の知識を仮定します。排他制御といった概念やミューテックス、セマフォといった同期のための機構についての知識を仮定します。
一部、発展的な内容に関する部分では、高校で習う程度の集合の記法(要素 x ∈ A, 部分集合 A ⊆ B など)を使います。
必要なもの
- ツール SyncStitch
- マウス
配布物と Zoom meeting URL
セミナー開始時刻までにCONNPASS のメッセージにてお知らせします。
同じメッセージを複数回送信する場合があります。あらかじめご了承ください。
使用するツール
CSP 理論に基づいたモデリングと検査が可能な SyncStitch というツールを使用します。
注意事項
- 配布スライド資料の公開は禁止です。配布モデルファイルはご自由にお使いください。
- 不測の事態が生じセミナーを開催または完遂できなかった場合は、日を改めて再開催することで対処させていただきます。
- 都合により申し込み後に参加できなくなった場合は、同等のセミナーを再演する際にご参加いただけるよう配慮しますのでご連絡ください。
参考書
- 並行システムの検証と実装
- Communicating Sequential Processes, C. A. R. Hoare
- The Theory and Practice of Concurrency, A.W. Roscoe
- Concurrent and Real-time Systems: The CSP Approach, Steve Schneider
- Understanding Concurrent Systems, A.W. Roscoe
連絡先
ご質問等がありましたら isaac@principia-m.com までお気軽にご連絡ください。
注意事項
※ 掲載タイミングや更新頻度によっては、情報提供元ページの内容と差異が発生しますので予めご了承ください。
※ 最新情報の確認や参加申込手続き、イベントに関するお問い合わせ等は情報提供元ページにてお願いします。