Principles of Concurrent and Distributed Programming
Chapter2 The Concurrent Programming Abstraction
2.1 Introduction
- ok
2.2 Interleaving
- 処理時間が違っても、処理順番が同じであれば同じと考える。
- システムの処理速度は時とともに変わってしまうので、それで動かなくなっては困るため。
- どのようなInterleaving(和訳語不明)のもとであろうと、並行プログラミングは正しく動くことを要求される。
- A concurrent program is required to be correct under all interleavings.
2.3 Atomic Instructions
- 次のようなプログラムが同時に走ったとき、正常に動作しない可能性がある。
x = 0; thread1 { for 10 times { x = x + 1; } } thread2 { for 10 times { x = x + 1; } } print x; => 20?
- それは、内部的にxを読み出し、加算し、代入する操作が分かれているため、
- Interleavingでは、この三つを不可分の操作として保障しないため。
- たとえば、
thread1 LOAD # x thread2 LOAD # x thread1 ADD # 1 thread2 ADD # 1 thread1 STORE # x thread2 STORE # x
-
- となった場合、xは1しか加算されない。
- 多くの環境ではより高レベルの命令(INCなど)がサポートされているのでそれを使う。
2.4 Correctness
- 部分的正当性(partial correctness)
- (P(a)∧terminates(Prog(a,b)))⊃Q(a,b)
- P(a)がtrueであって、計算が終了するなら、Q(a,b)が成り立ち、bに結果が入る。
- つまり、計算が終了しないこともありうる(常に答えが返ってくるとは限らない)。
- (P(a)∧terminates(Prog(a,b)))⊃Q(a,b)
- 完全正当性(total correctness)
- P(a)⊃(terminates(Prog(a,b))∧Q(a,b))
- P(a)がtrueなら、計算は終了し、かつQ(a,b)が成り立ち、bに結果が入る。
- つまり、計算が必ず終了することを要求する。
- P(a)⊃(terminates(Prog(a,b))∧Q(a,b))
- http://ja.wikipedia.org/wiki/%E6%AD%A3%E5%BD%93%E6%80%A7_%28%E8%A8%88%E7%AE%97%E6%A9%9F%E7%A7%91%E5%AD%A6%29
完全正当性(Total Correctness)は、アルゴリズムが常に停止することも要求される。
一方、部分正当性(Partial Correctness)は単に返ってくる答えが正しいことのみを要求する
(常に答えが返ってくるとは限らない)。
停止問題には汎用的解法はないので、完全正当性はより深い問題をはらんでいる。
- Safety properties
- 属性はいつも真でなければならない。(真が帰らなければならない)
- Safety propertiesには排他処理(mutex)などがある。
- Liveness properties
- 属性はいずれ必ず真にならなければならない(今現在も含まれる)
- Liveness propertiesは以下の状態がありうる。
- Weak fairness
- もしプロセスが、継続的にリクエストを出した状態を維持するなら、いつかはそれが付与されることは保障される
- Strong fairness
- もしプロセスが、無限にリクエスト出したり、取り下げたりしたとしても、いつかはそれが付与されることは保障される
- Linear waiting
- もしプロセスがひとつのリクエストを出すと、そのほかのプロセスのリクエストが二回以上付与される前に、それが付与される。
- FIFO (first-in first-out)
2.5 Inductive Proofs of Correctness
- 正当性の帰納的証明について
Basis
- Prove P(0).
Inductive step
- Assume that P(n) is true (the inductive hypothesis) and prove P(n+1).
- 基本的に以上のようなフォーマットで証明していけばいいとのこと。
Basis
- Prove the property for the initial state of the program.
Inductive step
- Assume that the property holds after the nth step of the execution sequence (the inductive hypothesis) and prove that it holds after the (n + 1)st step.
2.6 Liveness proofs
- Liveness propertiesの証明を簡単にやるが、実は厳密にやると、もっとずっと難しいんだとかなんとか。
- □p means p is always true.(いつも真)
- ◇p means p is eventually true.(いつか真)
- なら、◇□pと◇□qは◇□(p∧q)とあらわせる。
2.7 Further Reading
- もっと読みたい人へ。本(論文)へのリファレンスなどがある。
2.8 Exercises
- 1. 正しい答えを出す2.3のInterleavingsを列挙せよ。
thread1 LOAD # x thread1 ADD # 1 thread1 STORE # x thread2 LOAD # x thread2 ADD # 1 thread2 STORE # x ;または thread2 LOAD # x thread2 ADD # 1 thread2 STORE # x thread1 LOAD # x thread1 ADD # 1 thread1 STORE # x
- 2. 問題文がよくわからない。
- 3. 問題文がよくわからない。
- 4. 紙に□◇□pと◇□◇pの図を描け。描いた。
- 5. 以下は正しいか?
- (a) □(p∧q)⊃(□p∧□q) -> 正しい
- (b) (□p∧□q)⊃□(p∧q) -> 正しい
- (c) ◇(p∧q)⊃(◇p∧◇q) -> 正しい (?)
- (d) (◇p∧◇q)⊃◇(p∧q) -> 正しくない(◇□でない場合は途中で取り下げることができるため、タイミングが合わずに(p∧q)に成らない可能性もある)
- (e) □(p∨q)⊃(□p∨□q) -> 正しい
- (f) (□p∨□q)⊃□(p∨q) -> 正しい
- (g) ◇(p∨q)⊃(◇p∨◇q) -> 正しい (?)
- (h) (◇p∨◇q)⊃◇(p∨q) -> 正しい (?)