理論計算機科学を読むための数学・証明・アルゴリズム基礎

第13章 並行性と形式モデルの入口

章間ナビゲーション

この章で使う記号

記号 意味
S 状態集合
s → s' 状態 s から s' への遷移
trace 実行の列
□P 常に P が成り立つ
◇P いつか P が成り立つ
hb happens-before 関係
f 許容故障数として使われることが多い記号

この章で解消する詰まりどころ

並行計算では、普段のプログラム実行とは違い、複数の処理が同時に進みます。そこで次のような語が出ます。

state
transition
trace
nondeterminism
safety
liveness
linearizability
consensus

この章では、OSや分散システムの実装詳細ではなく、理論計算機科学で使う「状態と遷移による形式化」の最小限を扱います。

本体教科書で使う箇所

  • 並行計算: 共有メモリ、メッセージパッシング、プロセス代数、Petriネット。
  • 形式的検証: 状態遷移、到達可能性、安全性、活性、時相論理。
  • 分散システム理論: 合意問題、故障モデル、線形化可能性。
  • オートマトン: 状態集合、遷移関係、受理条件。

1. 状態

状態とは、システムの現在の状況を表す情報の組です。

例: 変数 x と y だけを持つプログラムなら、状態を次のように表せます。

(x=0, y=1)
(x=1, y=1)
(x=1, y=2)

状態は、必要な情報だけを抽象化して表します。メモリ全体を表す必要がある場合もありますが、証明に不要な詳細は落とします。

2. 遷移

遷移は、1つの状態から別の状態へ進むことです。

s -> s'

例:

(x=0) -> (x=1)

これは、プログラムが x := x + 1 を実行したことに対応します。

3. 遷移システム

遷移システムは、状態集合と遷移関係で構成されます。

T = (S, ->, s0)
  • S: 状態集合。
  • ->: 遷移関係。
  • s0: 初期状態。

到達可能状態とは、初期状態から0回以上の遷移で到達できる状態です。

4. 遷移関係と関数の違い

逐次的な決定的プログラムでは、次状態が1つに決まることがあります。

next: S -> S

しかし、並行計算や非決定的モデルでは、1つの状態から複数の次状態へ進めることがあります。

s -> s1
s -> s2

このため、遷移は関数ではなく関係として定義することが多いです。

5. 非決定性

非決定性とは、複数の遷移が可能であり、モデルがそのどれを選ぶかを固定しないことです。

重要なのは、非決定性は確率ではないという点です。

s -> s1
s -> s2

と書かれていても、s1 と s2 がそれぞれ1/2で選ばれる、という意味ではありません。どちらも可能である、という意味です。

6. interleaving

並行実行を扱う1つの方法は、各プロセスの1ステップ実行が任意の順序で交互に起こると考えることです。これを interleaving と呼びます。

例: 2つのプロセスがある。

P: a; b
Q: c; d

可能な interleaving の例:

a b c d
a c b d
c a d b
c d a b

ただし、各プロセス内の順序は保たれます。P では a が b より先、Q では c が d より先です。

7. trace

trace は、実行で観測されるイベント列です。

trace = a c b d

状態遷移をすべて見る代わりに、外部から観測されるイベント列だけを見ることがあります。

trace の集合としてシステムの振る舞いを定義すると、オートマトンやプロセス代数と接続しやすくなります。

8. safety

safety は「悪いことが起きない」という性質です。

例:

  • 2つのプロセスが同時にクリティカルセクションへ入らない。
  • 残高が負にならない。
  • 送信していないメッセージを受信しない。

safety は、有限の実行接頭辞で破れたことを確認できます。

悪い状態に到達しない

と表せることが多いです。

9. liveness

liveness は「良いことがいつか起きる」という性質です。

例:

  • 要求したプロセスは、いつか応答を受け取る。
  • ロックを待つプロセスは、いつかロックを獲得する。
  • 送信されたメッセージは、いつか配送される。

liveness は、有限の実行だけでは破れたと断定しにくい性質です。将来起きる可能性があるためです。

10. invariant

invariant は、到達可能なすべての状態で成り立つ性質です。

例:

x >= 0
queue の要素数 >= 0
token の総数は一定

safety の証明では、不変条件を使うことが多いです。

証明の型:

  1. 初期状態で invariant が成り立つ。
  2. invariant が成り立つ状態から1遷移しても invariant が保たれる。
  3. よって、すべての到達可能状態で invariant が成り立つ。

これは数学的帰納法と同じ構造です。

11. race condition

race condition は、実行順序によって結果が変わる問題です。

例: 共有変数 x=0 に対して、2つのスレッドが同時に x := x+1 を実行する。

各操作を細かく分けると、次のようになります。

read x
compute x+1
write x

2スレッドが interleaving されると、最終値が2ではなく1になる可能性があります。

12. 共有メモリモデル

共有メモリモデルでは、複数のプロセスが同じ変数やメモリ領域を読み書きします。

典型操作:

read(x)
write(x, v)
compare_and_swap(x, old, new)

共有メモリでは、同時アクセス、可視性、原子性、メモリ順序が問題になります。

13. メッセージパッシングモデル

メッセージパッシングモデルでは、プロセス同士がメッセージを送受信します。

典型操作:

send(p, m)
receive(p)

考慮すべき点:

  • メッセージが遅延するか。
  • メッセージが失われるか。
  • 順序が保たれるか。
  • プロセスが故障するか。

分散システム理論では、これらの仮定が結果を大きく変えます。

14. happens-before

happens-before は、イベント間の因果順序を表す関係です。

典型的には次が成り立ちます。

  1. 同じプロセス内では、プログラム順序が happens-before を作る。
  2. メッセージ送信は、そのメッセージ受信より happens-before。
  3. 推移律が成り立つ。

happens-before は全順序ではなく、半順序です。関係のない2つのイベントは、どちらが先とも決められません。

15. 線形化可能性の入口

並行オブジェクトが、外から見ると各操作がどこか一瞬で実行されたように見える性質を、線形化可能性と呼びます。

例: 並行キュー。

複数の enqueue と dequeue が重なって実行されても、各操作に線形化点を割り当てて、逐次キューの仕様と矛盾しない順序が作れるなら線形化可能です。

重要なのは、実際の実行時間区間と整合する逐次順序を作る点です。

16. 合意問題

合意問題では、複数のプロセスが値を提案し、全員が同じ値を決定することを目指します。

典型的な条件:

  1. 一致性: 2つの正しいプロセスが異なる値を決定しない。
  2. 妥当性: 決定値は、何らかのプロセスが提案した値である。
  3. 終了性: 正しいプロセスはいつか値を決定する。

分散システム理論では、故障モデルや同期性の仮定によって、合意が可能かどうかが変わります。

17. 故障モデル

故障モデルは、プロセスや通信路がどのように壊れるかの仮定です。

モデル 内容
crash failure プロセスが停止する
omission failure メッセージ送受信が欠落する
Byzantine failure 任意の不正な振る舞いをする

理論では、どの故障を許すかを明示しないと、主張が意味を持ちません。

18. 同期モデル

分散システムでは、時間に関する仮定も重要です。

モデル 内容
synchronous メッセージ遅延や処理時間に既知の上限がある
asynchronous メッセージ遅延や処理時間に既知の上限がない
partially synchronous ある時点以降など、限定的に同期的な仮定を置く

同じ合意問題でも、同期モデルにより可否が変わります。

19. Petriネットの入口

Petriネットは、場所、遷移、トークンで並行システムを表すモデルです。

  • place: 条件や資源を表す。
  • transition: イベントや動作を表す。
  • token: 現在存在する資源や状態を表す。

遷移は、入力 place に十分な token があるとき発火できます。発火すると、入力 place から token を消費し、出力 place に token を生成します。

Petriネットは、並行性、競合、同期、到達可能性を表すために使われます。

20. モデル検査の入口

モデル検査では、有限状態モデルが仕様を満たすかを機械的に調べます。

基本的な流れ:

  1. システムを状態遷移モデルとして表す。
  2. 仕様を論理式やオートマトンとして表す。
  3. 到達可能状態を探索する。
  4. 仕様違反があれば反例 trace を返す。

状態数は組合せ的に爆発します。これを state explosion と呼びます。

21. よくある誤り

誤り1: 並行性を単に「高速化」と考える

理論上の並行性の主要問題は、高速化ではなく、複数の動作の相互作用、非決定性、同期、故障、仕様の保存です。

誤り2: 非決定性を確率だと考える

非決定性は「どれも可能」という形式化であり、確率分布は与えません。

誤り3: safety と liveness を混同する

safety は悪いことが起きないこと。liveness は良いことがいつか起きることです。

誤り4: 分散システムの定理を故障モデル抜きで読む

分散システムの主張は、故障モデル、同期性、通信仮定に依存します。

22. 章末確認

次を説明できれば、この章の目的は達成です。

  1. 状態遷移システムを S, ->, s0 で定義できる。
  2. 非決定性と確率を区別できる。
  3. interleaving の考え方を説明できる。
  4. trace、safety、liveness を説明できる。
  5. invariant による safety 証明の型を説明できる。
  6. 共有メモリとメッセージパッシングの違いを説明できる。
  7. happens-before が半順序であることを説明できる。
  8. 合意問題の3条件を言える。

次に読む章

Edit this page on GitHub