並行システムの検証と実装第5章デッドロック検査 PRINCIPIA Limited 初谷久史 ©2015 PRINCIPIA Limited デッドロック検査 ● ● ミューテックスのモデルミューテックスによる排他制御 ● 2リソース問題 ● デッドロック検査 ● システムコールのモデル ● 抽象状態と継承 ● デッドロックの検出機構 ©2015 PRINCIPIA Limited ● ● プロセスが特定の状態にいることを観測する複数のプロセスがそれぞれ特定の状態に同時にいることを観測する 2 ミューテックスのモデル P0 lock0 unlock0 P1 lock1 unlock1 MUTEX P0 P1 lock unlock MUTEX クライアントごとにイベントを用意 ©2015 PRINCIPIA Limited インターリーブ結合 3 ミューテックス: クライアント毎 P0 lock0 unlock0 P1 lock1 unlock1 (define-event (define-event (define-event (define-event lock0) unlock0) lock1) unlock1) MUTEX どちらがロックしているか識別できる ©2015 PRINCIPIA Limited 4 ミューテックス: インターリーブ P0 P1 (define-event lock) (define-event unlock) lock unlock MUTEX 抽象化クライアントの識別不可 ©2015 PRINCIPIA Limited 5 共有メモリモデル P0 P1 rd wr (define-process P (? rd (x) (! wr ((+ x 1)) STOP))) (define-process (SHMEM m) (alt (! rd (m) (SHMEM m)) (? wr (x) (SHMEM x)) )) SHMEM m=1 m=2 ©2015 PRINCIPIA Limited 6 ミューテックスによる排他制御 P0 rd wr SHMEM ©2015 PRINCIPIA Limited P1 lock unlock MUTEX 7 インクリメントプロセスの修正 (define-process P (? rd (x) (! wr ((+ x 1)) STOP))) (define-process P (! lock (? rd (x) (! wr ((+ x 1)) (! unlock STOP))))) ©2015 PRINCIPIA Limited 8 インターリーブ結合 P0 P1 lock unlock rd wr SHMEM (define-process SYSTEM (par (list rd wr lock unlock) (par '() P P) (par '() (SHMEM 0) UNLOCK))) MUTEX まず相互作用のない P0 と P1， SHMEM と MUTEX をインターリーブで並行合成する P0 ||| P1 rd wr lock unlock SHMEM ||| MUTEX ©2015 PRINCIPIA Limited 2段階目の並行合成は左図のように見える（||| はインターリーブ結合を表す記号） 9 計算木 example-5-0-mutex.ss MUTEX がない場合 ©2015 PRINCIPIA Limited 10 † 2リソース問題 P0 P1 Scanner Printer ©2015 PRINCIPIA Limited プロセス P0, P1 それぞれが Scanner と Printer を同時に利用しようとしている MUTEX を2つ用意して排他制御を行う 11 2リソース問題 P0 lock0 unlock0 MUTEX0 ©2015 PRINCIPIA Limited P1 lock1 unlock1 MUTEX1 12 イベント定義 (define-event use0) (define-event use1) (define-event lock0) (define-event unlock0) プロセス P0, P1 それぞれが 2つの資源を同時に使うことを表すイベント (define-event lock1) (define-event unlock1) ©2015 PRINCIPIA Limited 13 プロセス定義: プロセスP0, P1 (define-process P0 (! lock0 (! lock1 (! use0 (! unlock1 (! unlock0 P0)))))) (define-process P1 (! lock1 (! lock0 (! use1 (! unlock1 ©2015 PRINCIPIA Limited (! unlock0 P1)))))) MUTEX0, MUTEX1 を順番にロックする資源の使用 P0 とは逆順にロック 14 プロセス定義: ミューテックス (define-process MUTEX0 (! lock0 (! unlock0 MUTEX0))) イベント以外は同じ (define-process MUTEX1 (! lock1 (! unlock1 MUTEX1))) cf. 以前に作成した状態遷移図バージョン ©2015 PRINCIPIA Limited 15 並行合成 (define-process SYSTEM (par (list lock0 unlock0 lock1 unlock1) (par '() P0 P1) (par '() MUTEX0 MUTEX1))) P0 lock0 unlock0 ©2015 PRINCIPIA Limited MUTEX0 P1 lock1 unlock1 MUTEX1 16 計算木 example-5-1-twores.ss P0 P1 MUTEX0 ©2015 PRINCIPIA Limited MUTEX1 17 † † デッドロック検査 Process list ウィンドウの "Assertions" ボタンを押すと Assertions ウィンドウが開く右クリックメニューから "add deadlock" を選択する ©2015 PRINCIPIA Limited 18 † デッドロック検査デッドロック検査式のテンプレートが表示されるのでプロセス名 P を SYSTEM に変える項目上で右クリックし "check" を選択する ©2015 PRINCIPIA Limited 19 デッドロック検査デッドロックが発見される記号の意味未検査問題なし問題あり ©2015 PRINCIPIA Limited 20 † デッドロックの分析項目上で右クリックし "explore" を選択する初期状態からデッドロック状態までの最短パスが表示されるデッドロックなので ©2015 PRINCIPIA Limited 遷移はない 21 † プロセスの修正 (define-process P0 (! lock0 (! lock1 (! use0 (! unlock1 (! unlock0 P0)))))) (define-process P1 (! lock0 (! lock1 (! use1 (! unlock1 ©2015 PRINCIPIA Limited (! unlock0 P1)))))) 同じ順序でロックする再検査デッドロックがないことが確認できる 22 デッドロック検査のポイント ● ● デッドロック検査の結果がならばいかなる実行パスにもデッドロックはないデッドロック検査の結果がだった場合初期状態からデッドロック状態への最短パスがわかるので，デッドロックが発生する原因を分析できる – プロセス木 – 環境 – サブプロセスの計算木 ©2015 PRINCIPIA Limited 23 ミューテックスのモデル P0 lock0 unlock0 P1 P0 lock1 unlock1 ret ret lock0 unlock0 P1 lock1 unlock1 MUTEX MUTEX システムコールのモデルクライアントごとにイベントを用意詳細 ©2015 PRINCIPIA Limited P0 P1 lock unlock MUTEX インターリーブ結合抽象 24 システムコールのモデルシステムコールのモデル P 抽象的な同期モデル MUTEX P lock lock ret 呼び出しとリターンをイベントで表現する（ret のみ待つという約束） ● ret イベント発生＝ロック獲得 ● クライアントがロックしようとしていることを lock で知る ● を返さないことでブロック ©2015ret PRINCIPIA Limited を表現できる MUTEX ● ● ● lockイベント発生＝ロック獲得クライアントがロックしようとしていることを知ることはできない 25 システムコール型ミューテックス ret イベントでロック獲得 P ロック中に Q がロック要求 P がロック中でかつ Q がロック要求している状態 ©2015 PRINCIPIA Limited unlock は単純なイベント同期 ● システムコール型と混在可能 26 ● 分析したい側面に注目する（抽象化）デッドロック検出機構目的: 実行時にデッドロックが発生したことを検出し回避する仕組みを考える資源要求 P R0 Q lock プロセス P0 所有 P1 R1 資源グラフ（R. C. Holt, 1972） ©2015 PRINCIPIA Limited MUTEX ret lock デッドロックを検出するにはクライアントが要求していることを識別する必要がある 27 2リソース問題再び P P.lock0 P.ret0 P.unlock0 Q.lock0 Q.ret0 Q.unlock0 MUTEX0 ©2015 PRINCIPIA Limited Q P.lock1 P.ret1 P.unlock1 Q.lock1 Q.ret1 Q.unlock1 MUTEX1 28 プロセス定義: プロセス P ©2015 PRINCIPIA Limited 29 プロセス定義: プロセスQ ©2015 PRINCIPIA Limited 30 問題設定 ● ミューテックスにデッドロック検出機構をつけプロセス P をそれに対応させることでデッドロックを回避できるようにすること ©2015 PRINCIPIA Limited 31 抽象状態と継承抽象状態は点線枠で表される抽象状態を作成し共通の状態変数を定義する変更が容易になる継承する状態を指定継承した変数が表示される ©2015 PRINCIPIA Limited 個別に変数を追加できる 32 抽象状態を使った MUTEX イベントを切り替えることで MUTEX0 と MUTEX1 になる ©2015 PRINCIPIA Limited 33 プロセス定義: MUTEX0, 1 (define-process MUTEX0 (LOCK P.lock0 P.unlock0 P.ret0 Q.lock0 Q.unlock0 Q.ret0)) (define-process MUTEX1 (LOCK P.lock1 P.unlock1 P.ret1 Q.lock1 Q.unlock1 Q.ret1)) ©2015 PRINCIPIA Limited 34 並行合成 (define X (list P.lock0 P.lock1 Q.lock0 Q.lock1 P.unlock0 P.unlock1 Q.unlock0 Q.unlock1 P.ret0 P.ret1 Q.ret0 Q.ret1)) (define-process SYSTEM (par X (par '() P Q) (par '() MUTEX0 MUTEX1))) ©2015 PRINCIPIA Limited P Q MUTEX0 MUTEX1 35 † デッドロック検査 example-5-2-mutex-syscall.ss ©2015 PRINCIPIA Limited 36 デッドロックの検出 MUTEX0 (R0) 資源グラフ R0 P Q R1 MUTEX1 (R1) Q は R0 を所有かつ R1 を要求中 P は R1 を所有かつ R0 を要求中 ©2015 PRINCIPIA Limited この2つの状態に同時にいると 37 デッドロックデッドロックの検出 MUTEX0 (R0) 資源グラフ R0 P Q R1 MUTEX1 (R1) ©2015 PRINCIPIA Limited 逆順のケース 38 プロセスが特定の状態にいることを観測する方法出入りイベントを観測する状態にいることを知らせるイベントを追加して観測する ©2015 PRINCIPIA Limited 39 状態観測用イベントを追加 ©2015 PRINCIPIA Limited 40 "同時"にいることの観測 MUTEX0 対応する2つの遷移に同じイベントを指定し同期させて観測する（マルチ同期） MUTEX1 ©2015 PRINCIPIA Limited 41 デッドロック検出機構: MUTEX (define-event detected0) (define-event detected1) 観測用イベント定義 (define-process MUTEX0 (LOCK P.lock0 P.unlock0 P.ret0 Q.lock0 Q.unlock0 Q.ret0 detected0 detected1)) (define-process MUTEX1 (LOCK P.lock1 P.unlock1 P.ret1 Q.lock1 Q.unlock1 Q.ret1 detected1 detected0)) ©2015 PRINCIPIA Limited 逆順 42 デッドロック検出機構: SYSTEM (define X (list P.lock0 P.unlock0 P.ret0 P.lock1 P.unlock1 P.ret1 Q.lock0 Q.unlock0 Q.ret0 Q.lock1 Q.unlock1 Q.ret1 detected0 detected1)) MUTEX‒P 間で同期 (define-process SYSTEM (par X MUTEX0−1 間で同期 (par '() P Q) (par (list detected0 detected1) MUTEX0 MUTEX1))) ©2015 PRINCIPIA Limited 43 デッドロック検出機構: P ©2015 PRINCIPIA Limited 44 † デッドロック検査・計算木 example-5-3-dldetect.ss ©2015 PRINCIPIA Limited 45 デッドロック検査まとめ ● デッドロック検査 – デッドロックが存在しないことを確認できる – 初期状態からデッドロック状態への最短パスがわかる ©2015 PRINCIPIA Limited 46 デッドロック検査まとめ ● ミューテックスのモデル ● 2リソース問題 – ● デッドロックを避けるにはロックの獲得順序を統一するシステムコールのモデル – 呼び出しとリターンを表すイベントを導入 ©2015 PRINCIPIA Limited 47 デッドロック検査まとめ ● 抽象状態と継承 – ● ● 状態変数の定義を集中してメンテナンスしやすくするプロセスが特定の状態にいることを観測する – 出入りイベントを観測する – 状態にいることを通知するイベントを導入し観測する複数のプロセスがそれぞれ特定の状態に同時にいることを観測する – マルチ同期を使用する ©2015 PRINCIPIA Limited 48