Alloyでピーターソンのアルゴリズム
ピーターソンのアルゴリズムは、通信のために共有メモリだけを使い「2個」のプロセス間でリソースを競合することなく共有する相互排他のためのアルゴリズムである。
Alloyでモデリングしてみた。 https://github.com/nishio/learning_alloy/blob/master/Peterson.als
Wikipediaに書いてある「P0とP1は決して同時にクリティカルセクションには入らない。」を検証してみよう。for 15 Timeのスコープで2つのプロセスのプログラムカウンタが同時に3(つまりクリティカルセクション内)にならないことを検証させる。反例は見つからない。
check MutualExclusion {
no t: Time {
PC.proc[0].t = 3
PC.proc[1].t = 3
}
} for 15 Timeじゃあ「プロセスはクリティカルセクション1回分の処理時間以上に待たされることはない」も検証してみよう。やってみたらさくっと反例が見つかった。
check BoundedWaiting_Bad {
no t: Time, pid: Int {
PC.proc[pid].t = 2
PC.proc[pid].(t.next) = 2
PC.proc[pid].(t.next.next) = 2
PC.proc[pid].(t.next.next.next) = 2
PC.proc[pid].(t.next.next.next.next) = 2
}
} for 15 Time理由は割と簡単で「各時刻にどちらかのプロセスが1ステップ実行される」という仕様では「自分は『進める状態』相手が『待たされる状態』で、相手プロセスが5回連続で実行される」が起こりうるから。「各時刻1個につき、ランダムに選ばれた片方のプロセスが1ステップ実行される」という条件ではランダムに選ばれた結果 「待つべき側のプロセスばかり連続して実行される(その結果何も変わらない)」が起こるわけだ。
だからWikipediaの 「プロセスはクリティカルセクション1回分の処理時間以上に待たされることはない」 を文字通りに捉えたのが間違い。たとえば「あるプロセスが待っている間に片方のプロセスが2回連続してクリティカルセクションを実行することはない」とするべき。よし、これならfor 15 Timeのスコープで反例はない。
check BoundedWaiting {
no t, t': Time, pid: Int {
let range = Time - t.prevs - t'.nexts {
// あるプロセスがずっと2(ロック待ち)で
all t'': range | PC.proc[pid].t'' = 2
// その間、もう片方のプロセスが2回以上3(クリティカルセクション)を実行
#{t'': range |
PC.proc[PC.current_pid.t''].t'' = 3
} >= 2
}
}
} for 15 Time
アウトオブオーダー実行
さてさて、ここからが本題なのだが、ピーターソンのアルゴリズムは命令が書かれた順序で実行されることを想定している。現代のCPUはそうではない*1。だから現代のCPUで動くようにするには適切にフェンスを置く必要がある*2。
で、光成さん*3に色々教えてもらいながらgcc -S -O3 -fomit-frame-pointer tmp.cしたり#include
というわけで実機で試しても何も安心できないので、今後Alloyでアウトオブオーダー実行をモデリングしようと思うんだけど、とりあえず手始めに0行目と1行目のstoreが入れ替わったらどうなるか試してみたらさくっと2.5秒でクリティカルセクションに両方が入る反例が見つかった。
Time$1: pc0=0, pc1=1, pid=1 turn=0 f0=0 f1=0 // p1がturnを0にする Time$2: pc0=1, pc1=1, pid=0 turn=1 f0=0 f1=0 // p0がturnを1にする Time$3: pc0=2, pc1=1, pid=0 turn=1 f0=1 f1=0 // p0がf1==0だから「p1は待っていない」と判断、進入 Time$4: pc0=3, pc1=1, pid=0 turn=1 f0=1 f1=0 Time$5: pc0=3, pc1=2, pid=1 turn=1 f0=1 f1=1 // p1が「turnが1だから俺が進んでよい」と判断、進入 Time$6: pc0=3, pc1=3, pid=1 turn=1 f0=1 f1=1 // ここで両方ともクリティカルセクション(pc=3)にいる Time$7: pc0=3, pc1=0, pid=1 turn=1 f0=1 f1=0 Time$8: pc0=0, pc1=0, pid=0 turn=1 f0=0 f1=0 Time$9: pc0=1, pc1=0, pid=0 turn=1 f0=0 f1=0
だから0行目と1行目の間には最低限sfenceは必要なわけだな。
追記: 「sfenceが必要」と書いたのは言いたかったことを正確に表現できていないということがわかった。see melancholic afternoon。「アウトオブオーダー実行でW→Wの順序を入れ替える可能性のあるCPUでピーターソンのアルゴリズムを動かす場合、0行目と1行目の間にはW→Wの順序を保つ制約を入れる必要がある」と言うべきだった。Core 2 Duo, Atom, Core Duo, Pentium 4, P6ではW→Wの順序は(一部の命令を除いて)保存されるのでsfenceを入れる必要もないようだ。
次回予定: 「Alloyでアウトオブオーダー実行」
