Mutual exclusion
Mutual exclusion”相互排他”とは、とあるアルゴリズムで１つのリソースが複数のスレッドによって同時に変更されることがないことである。
この章の目標
相互排他を証明する推論の種類を知る。また、ロックアルゴリズムを少し解説。その際、コンピュータアーキテクチャのことはこの章では無視する。
記法
a0 →a1 // a0はa1に先行して開始する
I(a0, a1) // a0, a1間のインターバル
IA = I(a0, a1), IB = (b0, b1)の時、IA → IB // インターバルIAがIBに先行する
2つのイベントが→で表せない場合、それらのイベントは並列である。
a, I(b0, b1)がある時、a→b1ならばa→Iである。また、b1→aならばI→aである
良い並列アルゴリズムが満たす３つの性質
- Mutual exclusive
- 当たり前。これが満たされなければ正しい計算結果は得られない
- Deadlock-free
- 必ずプログラムが終了することを保証する。
- Starvation-free
- ロックされていなければ、クリティカルセクションに待たずに入れることを保証する。
The Peterson Lock
2スレッド間の排他制御を達成するロック方式。
相互排他の証明
クリティカルセクションに入る条件は、この待機ループが抜けることです。
つまり、 flag[other] == false または turn != other のどちらかが成り立つ必要があります。
矛盾を証明することで、両方のスレッドが同時にクリティカルセクションに入ることはないと示します。
仮定： 両方のスレッド (P0 と P1) が同時にクリティカルセクションに入る
P0がlock(0)を呼び、flag[0] = trueになり、turn = 1になる。P1がlock(1)を呼び、flag[1] = trueになり、turn = 0になる。P0がクリティカルセクションに入るには、while (flag[1] && turn == 1);を抜ける必要がある。- しかし、
flag[1] = trueであり、turn = 0なので、この条件は満たされない → P0 は待機する
- しかし、
P1も同様にwhile (flag[0] && turn == 0);を抜ける必要がある。- しかし、
flag[0] = trueであり、turn = 1なので、この条件は満たされない → P1 も待機する
- しかし、
したがって、両方のスレッドが同時にクリティカルセクションに入ることは不可能である。
相互排他は保証される ✅
デッドロックなし (Deadlock-Free) の証明
デッドロックが発生しないことを証明するには、少なくとも1つのスレッドがクリティカルセクションに進むことができることを示せばよい。
証明
- あるスレッド (
P0) がwhile (flag[1] && turn == 1);のループに入っていると仮定する。 - しかし、
P1がunlock(1)を呼び出すと、flag[1] = falseになる。 - すると、
while (false && turn == 1);となるため、P0はループを抜けてクリティカルセクションに進める。
同様に P1 についても同じ議論が成り立つため、デッドロックは発生しない。
デッドロックは起こらない ✅
3. 公平性 (Fairness, Starvation-Free) の証明
公平性とは、「どちらのスレッドも無限に待たされることはない」ことを意味します。
証明
turn変数は、クリティカルセクションに入る直前に相手 (other) に譲られる。- そのため、次にクリティカルセクションに入りたいスレッド (
other) は、すでにturn == otherになっている。 otherのスレッドがunlock()した後は、待機中のスレッドがすぐにwhile()を抜けて進める。
つまり、どちらかのスレッドがクリティカルセクションを出ると、もう片方のスレッドが進行可能になるため、無限に待たされることはない。
公平性が保証される ✅
Filter Lock
Peterson Lockを一般化しn個のスレッドで相互排他可能なロック。
TODO: 証明を記述
Lamport’s Bakery algorithm
first-come-first-serve→先にロックを呼んだスレッドが先にクリティカルセクションを実行することを保証するロック要件を満たすロックアルドリズム。
コメント