TAoMPのLockOneクラス

The Art of Multiprocessor Programming 並行プログラミングの原理から実践まで」を少しずつ読んでいる。
まだ最初の方しか読んでいないが、証明は読みなれないので骨が折れる。正しい理解かどうかはわからないが、とりあえずメモ。

LockOneクラスの Lemma 2.3.1 の証明の想定は何を言ってるのかわかりにくいが、CS_Aが終わる前にCS_Bが始まる(またはその逆)ことがあると想定する、ということ。jとかkは証明には出てこないが、こういう言い方がカッコいいのだろう。


式 2.3.4 は、その想定から出てくるもので、

write_A(flag[A] = true) \to read_A(flag[B] == false) \to

の後はCS_Aになるはずだが、仮定によればCS_Bに入ることができるので、

write_B(flag[B] = true) \to read_B(flag[A] == false)

となることがある(本にある言葉でいうと、そのようなjとkが存在する)。lock()メソッドだけでは一度trueにしたものはfalseにはならないのに、flag[A] が false に戻っているので、矛盾しているというわけだ。


unlock() を使うのはCSの終わりを意味するが、今考えているのはCSが終わる前のことだけだから、unlock()は気にしない。

8ページの、AliceとBobのたとえ話と話の流れは同じだ。スレッドAがAliceでスレッドBがBob。flagは旗。CSは庭。

Mutual Exclusion Companion slides for The Art of (3)に少し違う方法が書かれている。より難しいやり方のように見える。