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に結果が入る。
      • つまり、計算が終了しないこともありうる(常に答えが返ってくるとは限らない)。
  • 完全正当性(total correctness)
    • P(a)⊃(terminates(Prog(a,b))∧Q(a,b))
      • P(a)がtrueなら、計算は終了し、かつQ(a,b)が成り立ち、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)
      • FIFOは有名、はじめに入れられたものがはじめに出る。普通の順番待ち。
      • FIFOがもっとも強い公平性を持っている的な説明
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) -> 正しい (?)