AlloyでDining Philosophers 〜その２: デッドロックを検出しよう〜

形式手法 モデル検証

さて、この前の日記で、哲学者たちとフォークを一つのテーブルに着かせる事ができました。
では、今度はナイーブなアルゴリズムでデッドロックが起きる事を検証してみましょう。

今回のアルゴリズム

  • 哲学者は同時に１本のフォークをとる。
  • ２本獲得して満足したら２本同時に手放す。
  • 哲学者はとってもグリーディなので、１本握ったら、食べるまでそれを離さない。

Alloyで記述してみる。

まずは、システムのグローバルな状態を定義して、その状態間の関係を定義することで、アルゴリズムの実行を記述します。
今回は簡単の為にフォーク自体の排他制御は仮定した上で、「フォークが誰に持たれているか」を追う事にしましょう。

-- Global State
sig State {
        -- フォークの保持者は高々一人(lone:least or equal to one)
	owned: Fork -> lone Philosopher
}{
	-- フォークは自分の両脇の哲学者からしか保持されない
	-- f.ownedでも良いが、ボックス結合を使って読みやすく(a.bをb[a]って書ける)
	all f:Fork | owned[f] in f.(left+right)
}

あとは、この状態間の関係を定義してやればいい訳ですね。
とその前に、ちょっと記述を読みやすくするために述語を導入しておきます。

-- フォークの為の述語
-- ある状態sでフォークfはフリーである（誰にも保持されていない）
pred free ( s: State, f: Fork ) {
	no s.owned [ f ]
}

-- 哲学者の為の述語
-- ある状態sで哲学者pは食べている（両隣のフォークの保持者がpである）
pred eating ( s: State, p: Philosopher ) {
	p  = s.owned[p.rightFork] and p =  s.owned[p.leftFork]
}

さて、準備は整いました。「状態間の関係」を定義してみます。具体的に言うと、

ある状態sである哲学者が左のフォークを取ると状態s'になる

みたいな事です。
これをAlloyで書いてみます。今回は状態間の遷移で、誰か一人しか動かないと仮定します。

-- 状態sで哲学者pが左のフォークを取った状態がs'である
pred TakeLeft ( s: State, s': State, p: Philosopher ) {
	-- sではpの左のフォークは空いていて、s'ではpの左のフォークはpが保持している
	-- (述語に引数を適用する場合には[]を使う)
	free[s,p.leftFork] and s'.owned[p.leftFork] = p
	-- それ以外のフォークは保持者が変化していない
	and (all f: (Fork - p.leftFork) | s.owned[f] = s'.owned[f])
}

こんな風に右のフォークを取る場合、食べてる時に両方のフォークを離すを記述してみると、校鳴ります。

-- 状態sで哲学者pが右のフォークを取った状態がs'である
pred TakeRight ( s: State, s': State, p: Philosopher ) {
	free[s,p.rightFork] and s'.owned[p.rightFork] = p
	and (all f: (Fork - p.rightFork) | s.owned[f] = s'.owned[f])
}
-- 状態sで哲学者pが食べていて、両方のフォークを手放した状態がs'である。
pred Release(s:State, s':State, p:Philosopher){
	eating[s,p] and (free[s',p.rightFork] and free[s',p.leftFork])	
	and (all f: (Fork - (p.leftFork + p.rightFork)) | s.owned[f] = s'.owned[f])
}

さて、後は、「初期状態」と「次の状態」を定義してやれば、状態が時系列に並びますね。その並んだ状態列の中で、デッドロック、つまり、全員がどのアクションも取る事ができない状態があるかどうかを調べます。
Alloyでは任意のシグネチャ(sigで定義したやつ)に全順序を導入してくれるモジュールが用意されていますので、それを使います。

open util/ordering[State]

って書いておくと、Stateに全順序を導入してくれて, first,next[s],lastなんていうので状態にアクセスできます。
これを用いて、アルゴリズムの実行を、State間の順序の制約として記述します。

-- 初期状態の述語
pred init ( s: State ) {
	all f: Fork | free [ s, f ]
}
-- 状態上の全順序に与える制約
fact Traces {
	-- firstはinitを満たす
	init [ first ] 
	-- 最後の状態以外の状態sは
	-- 誰かが動作できる状態ならsの次の状態next[s]は誰かが動いた後の状態であり、
	-- かつ、そう出なければ、何も変わっていない(デッドロックが続いている)
	all s: State - last
		| SomeoneCanMove[s] => SomeoneActioned[s,next[s]] else s.owned = next[s].owned
} 
-- 状態sで、誰かが動いた状態がs'である。
pred SomeoneActioned ( s: State, s': State ) {
	some p: Philosopher | TakeLeft [ s, s', p ] or TakeRight [ s, s', p ] or Release[s,s',p] 
}
-- 状態sで誰かが動作できる。
pred SomeoneCanMove(s:State){
	some p: Philosopher | 
		free[s,p.leftFork] or free[s,p.rightFork] or eating[s,p]
}

さて、これで記述が終わりました。Alloyにデッドロックに陥るまでの実行を検出してもらいましょう。

-- デッドロックが存在する実行である
pred WithDeadLock{
	-- ある状態sは、初めてのデッドロック状態で、その後ずっとデッドロック。
	some s:State | not SomeoneCanMove[s] 
				and all s': s.^next | not SomeoneCanMove[s'] -- s以降のs'はずっとデッドロック
				and all s'': s.^prev | SomeoneCanMove[s''] -- s以前はずっと誰かが動ける
}
-- デッドロックが存在する実行を見つけてくれ、というコマンド。
-- 3フォーク、3人の哲学者、実行の長さは10ステップ
run WithDeadLock for exactly 3 Fork, 3 Philosopher,  10 State

これを実行するとこんな感じの状態が出てきます。（Stateプロジェクションを利用したり不要な関係は表示しないようにしてあります。)

確かにデッドロックが検出できていますね。３人が同じ方のフォークを握ってしまった瞬間誰もはなせなくなる、というのが発見できました。

タイムアウトをつけたりすると、デッドロックは起きなくなりますが、今度はスタベーションが起きたりしてきます。
いろんな制約をつけて実行を探させても面白いですね。

今回使ったスクリプトをココに置いておきます。