第12章 並行計算の理論
はじめに
並行計算の理論は、複数の計算プロセスが同時に実行される状況を数学的に扱う分野です。マルチコアプロセッサ、分散システム、クラウドコンピューティングの普及により、並行性の理解と制御は現代のコンピュータサイエンスにおいて不可欠となっています。本章では、並行システムのモデル化、解析、検証のための理論的基礎を体系的に学びます。
並行性がもたらす非決定性、デッドロック、競合状態などの問題は、逐次プログラムでは現れない固有の複雑さを持ちます。これらの問題を理解し、解決するための形式的手法は、信頼性の高い並行システムの設計に欠かせません。本章で学ぶ理論は、オペレーティングシステム、データベース、分散アルゴリズムなど、幅広い分野の基礎となります。
12.1 並行計算モデル
12.1.1 並行性の基本概念
graph TD
subgraph "並行計算の基本概念"
subgraph "並行性 vs 並列性"
Concurrency["並行性（Concurrency）<br/>・論理的な同時性<br/>・単一CPUでもインターリーブ<br/>・非決定性あり"]
Parallelism["並列性（Parallelism）<br/>・物理的な同時実行<br/>・複数CPU/コア<br/>・性能向上が目的"]
Both["両方の組み合わせ<br/>・マルチコアでの並行実行<br/>・分散システム"]
end
subgraph "実行モデルの比較"
Sequential["逐次実行<br/>A1 → A2 → A3<br/>B1 → B2 → B3"]
Interleaved["インターリーブ実行<br/>A1 → B1 → A2 → B2 → A3 → B3<br/>または<br/>B1 → A1 → B2 → A2 → B3 → A3"]
Parallel_Exec["並列実行<br/>A1 || B1<br/>A2 || B2<br/>A3 || B3"]
end
subgraph "通信パラダイム"
SharedMem["共有メモリ<br/>・共通変数へのアクセス<br/>・同期プリミティブ<br/>・競合状態の問題"]
MessagePass["メッセージパッシング<br/>・send/receive操作<br/>・チャネル通信<br/>・デッドロックの問題"]
Actor["アクターモデル<br/>・独立したアクター<br/>・非同期メッセージ<br/>・局所状態のみ"]
end
subgraph "並行システムの問題"
RaceCondition["競合状態<br/>・共有データへの非同期アクセス<br/>・実行順序に依存した結果<br/>・再現困難なバグ"]
Deadlock["デッドロック<br/>・相互に待機状態<br/>・循環的な資源依存<br/>・システム停止"]
Starvation["飢餓状態<br/>・一部プロセスが永続的に待機<br/>・優先度による不公平<br/>・進行不能"]
end
end
style Concurrency fill:#e3f2fd
style Parallelism fill:#fff3e0
style SharedMem fill:#e8f5e8
style MessagePass fill:#f3e5f5
style RaceCondition fill:#ffebee
style Deadlock fill:#ffebee
定義 12.1 並行システムは、複数のプロセスが同時に実行される可能性があるシステム。
並行性 vs 並列性：
- 並行性（Concurrency）：論理的な同時性、インターリーブ実行を含む
- 並列性（Parallelism）：物理的な同時実行
インターリーブ意味論： 並行実行を、可能なすべての実行順序（インターリーブ）の集合として捉える。
12.1.2 共有メモリモデル
定義 12.2 共有メモリシステムでは、プロセスが共通の変数を通じて通信する。
原子的操作：
- Read：x の値を読む
- Write：x に値を書く
- Read-Modify-Write：Test-and-Set、Compare-and-Swap
メモリ一貫性モデル：
- 逐次一貫性（Sequential Consistency）
- 弱い一貫性モデル（TSO、PSO、Relaxed）
12.1.3 メッセージパッシングモデル
定義 12.3 メッセージパッシングシステムでは、プロセスがメッセージ送受信により通信する。
通信プリミティブ：
- send(p, m)：プロセス p にメッセージ m を送信
- receive(q)：プロセス q からメッセージを受信
同期性：
- 同期通信：送信と受信が同時に起こる
- 非同期通信：送信後、受信まで遅延がある
12.2 プロセス代数
12.2.1 CCS（Calculus of Communicating Systems）
定義 12.4 CCS の構文：
P ::= 0 (停止)
| α.P (プレフィックス)
| P + Q (選択)
| P | Q (並行合成)
| P\L (制限)
| P[f] (リラベリング)
| A (プロセス定数)
アクション：
- a, b, c, …：入力アクション
- ā, b̄, c̄, …：出力アクション
- τ：内部アクション
12.2.2 操作的意味論
遷移規則（構造的操作意味論）：
(Act) α.P --α--> P
(Sum1) 前提: P --α--> P'
結論: P + Q --α--> P'
(Par1) 前提: P --α--> P'
結論: P | Q --α--> P' | Q
(Com) 前提: P --a--> P', Q --ā--> Q'
結論: P | Q --τ--> P' | Q'
12.2.3 双模倣等価性
定義 12.5 関係 R が双模倣（bisimulation）であるとは： P R Q ならば、
- P –α–> P’ ⇒ ∃Q’, Q –α–> Q’ かつ P’ R Q’
- Q –α–> Q’ ⇒ ∃P’, P –α–> P’ かつ P’ R Q’
定義 12.6 P と Q が双模倣等価（P ∼ Q）⟺ ある双模倣 R で P R Q
定理 12.1 双模倣等価性は合同関係である（すべての文脈で保存される）。
12.2.4 その他のプロセス代数
CSP（Communicating Sequential Processes）：
- 失敗意味論
- トレース、失敗、発散
π計算：
- 名前の移動性
- チャネルを値として送受信可能
12.3 Petri ネット
12.3.1 基本定義
graph TD
subgraph "Petriネットによる並行システムモデリング"
subgraph "基本要素"
Places["プレース（○）<br/>・状態や条件を表す<br/>・トークンを保持<br/>・例：リソース、状態"]
Transitions["トランジション（□）<br/>・イベントやアクションを表す<br/>・発火により状態変化<br/>・例：プロセス実行、操作"]
Arcs["アーク（→）<br/>・プレースとトランジションを接続<br/>・重みを持つ<br/>・トークンフロー"]
Tokens["トークン（●）<br/>・プレース内のリソース数<br/>・システムの現在状態<br/>・マーキング M(p)"]
end
subgraph "相互排除の例"
P1["プロセス1<br/>待機"]
P2["プロセス2<br/>待機"]
Resource["共有リソース<br/>●"]
CS1["プロセス1<br/>クリティカル"]
CS2["プロセス2<br/>クリティカル"]
T1["リソース<br/>取得1"]
T2["リソース<br/>取得2"]
T3["リソース<br/>解放1"]
T4["リソース<br/>解放2"]
P1 --> T1
T1 --> CS1
CS1 --> T3
T3 --> P1
T1 --> Resource
Resource --> T1
P2 --> T2
T2 --> CS2
CS2 --> T4
T4 --> P2
T2 --> Resource
Resource --> T2
end
subgraph "発火規則"
EnableRule["発火可能条件<br/>すべての入力プレースに<br/>十分なトークンがある"]
FireRule["発火効果<br/>1. 入力からトークン除去<br/>2. 出力にトークン追加<br/>3. 原子的に実行"]
Example["例：t が発火可能<br/>•t = {p1, p2}<br/>M(p1) ≥ 1, M(p2) ≥ 1"]
end
subgraph "解析可能な性質"
Reachability["到達可能性<br/>・特定の状態に到達可能か<br/>・R(N, M₀) の計算"]
Boundedness["有界性<br/>・トークン数に上限があるか<br/>・メモリ使用量の保証"]
Liveness["活性<br/>・デッドロックの回避<br/>・すべてのトランジション発火可能"]
Invariants["不変量<br/>・P-不変量：場所の線形結合<br/>・T-不変量：遷移の発火回数"]
end
end
style Places fill:#e3f2fd
style Transitions fill:#fff3e0
style Resource fill:#ffebee
style Reachability fill:#e8f5e8
style Liveness fill:#f3e5f5
定義 12.7 Petri ネットは5つ組 N = (P, T, F, W, M₀)：
- P：プレース（場所）の有限集合
- T：トランジション（遷移）の有限集合（P ∩ T = ∅）
- F ⊆ (P × T) ∪ (T × P)：フロー関係
- W: F → ℕ₊：重み関数
- M₀: P → ℕ：初期マーキング
12.3.2 実行意味論
定義 12.8 トランジション t が発火可能 ⟺ ∀p ∈ •t, M(p) ≥ W(p, t)
発火規則：t が発火すると、マーキングは以下のように変化：
- ∀p ∈ •t: M’(p) = M(p) - W(p, t)
- ∀p ∈ t•: M’(p) = M(p) + W(t, p)
- その他：M’(p) = M(p)
12.3.3 性質解析
到達可能性： 初期マーキング M₀ から到達可能なマーキングの集合 R(N, M₀)。
構造的性質：
- 有界性：∀M ∈ R(N, M₀), ∀p ∈ P, M(p) ≤ k
- 安全性：1-有界性
- 活性：すべての到達可能マーキングから各トランジションが発火可能
不変量：
- P-不変量：Y^T · C = 0 を満たすベクトル Y
- T-不変量：C · X = 0 を満たすベクトル X
（C は接続行列）
12.3.4 解析手法
可達木： 到達可能なマーキングを木構造で表現。無限の場合は ω を使用。
線形代数的手法： 状態方程式：M = M₀ + C · σ（σ は発火回数ベクトル）
定理 12.2 M が到達可能ならば状態方程式を満たす（逆は一般に不成立）。
12.4 時相論理による並行システムの検証
12.4.1 並行システムの性質
安全性（Safety）：”悪いことは起こらない”
- 相互排除：同時にクリティカルセクションに入らない
- 部分正当性：終了すれば正しい結果
活性（Liveness）：”良いことがいつか起こる”
- 無飢餓性：要求したプロセスはいつかリソースを得る
- 全域的進行：システム全体が進行する
公平性（Fairness）：
- 弱公平性：永続的に可能な動作はいつか実行される
- 強公平性：無限回可能な動作はいつか実行される
12.4.2 CTL による検証
並行システムのモデル化： Kripke 構造 M = (S, S₀, R, L)
- S：状態集合
- S₀：初期状態集合
- R：遷移関係
- L：ラベリング関数
典型的な性質の記述：
- 相互排除：AG ¬(critical₁ ∧ critical₂)
- 応答性：AG (request → AF grant)
- 無飢餓：AG (request → AF critical)
12.4.3 モデル検査アルゴリズム
状態爆発問題： プロセス数に対して状態数が指数的に増加。
対策：
- シンボリックモデル検査（BDD を使用）
- 有界モデル検査（SAT ソルバを使用）
- 抽象化技法
12.5 分散アルゴリズム
12.5.1 分散システムのモデル
システムモデル：
- プロセス故障：クラッシュ、ビザンチン
- 通信：同期、非同期
- ネットワーク：完全グラフ、任意トポロジー
複雑性尺度：
- メッセージ複雑度
- 時間複雑度（ラウンド数）
- 空間複雑度（局所）
12.5.2 基本的な分散アルゴリズム
リーダー選出
LCR アルゴリズム（リング上）：
各プロセス p：
1. 自分の ID を右隣に送信
2. 受信した ID が自分より大きければ転送
3. 自分の ID を受信したらリーダー
メッセージ複雑度：O(n²)
時間複雑度：O(n)
HS アルゴリズム： 双方向リング、フェーズごとに距離を倍増 メッセージ複雑度：O(n log n)
相互排除
Lamport のベーカリーアルゴリズム：
プロセス i がクリティカルセクションに入る：
1. choosing[i] = true
2. number[i] = max(number[0], ..., number[n-1]) + 1
3. choosing[i] = false
4. 各 j ≠ i に対して：
- choosing[j] = false を待つ
- (number[j] = 0) または
(number[i], i) < (number[j], j) を待つ
5. クリティカルセクション
6. number[i] = 0
12.5.3 合意問題
定義 12.9 合意問題の要件：
- 合意：すべての正常プロセスは同じ値を出力
- 妥当性：出力値は入力値の一つ
- 停止性：正常プロセスは有限時間で出力
Byzantine 将軍問題
定理 12.3 n 個のプロセスのうち f 個が Byzantine 故障の場合、 合意が可能 ⟺ n > 3f
証明の概要（不可能性、n ≤ 3f）： 3プロセスで1つが故障の場合を考える。対称性により矛盾を導く。□
FLP 不可能性定理
定理 12.4（Fischer-Lynch-Paterson） 非同期システムでは、1つのプロセス故障でも決定的合意は不可能。
証明の概要：
- 2つの決定値の「境界」となる構成が存在
- その構成から1ステップで決定が変わる
- 故障により決定を遅延させ続けることが可能□
12.5.4 分散スナップショット
Chandy-Lamport アルゴリズム： 一貫性のある大域状態を記録
アルゴリズム：
- 開始プロセスが自状態を記録し、マーカーを送信
- マーカー受信時：
- 初回：自状態を記録、マーカーを転送
- 2回目以降：チャネル状態を記録
性質：記録される状態は、実際の計算で起こりうる状態。
12.6 並行データ構造
12.6.1 ロックベースの手法
粗粒度ロック： データ構造全体に1つのロック。単純だが並行性が低い。
細粒度ロック： 各ノードにロック。高い並行性だが、デッドロックの危険。
ハンドオーバーハンドロック： リストやツリーの走査で、次のノードをロックしてから現在のノードを解放。
12.6.2 ロックフリーアルゴリズム
graph TD
subgraph "並行データ構造の設計手法"
subgraph "ロックベース vs ロックフリー"
LockBased["ロックベース<br/>・排他制御により安全性確保<br/>・デッドロック、優先度逆転<br/>・コンテキストスイッチオーバーヘッド"]
LockFree["ロックフリー<br/>・CAS等の原子的操作<br/>・システム全体の進行保証<br/>・ABA問題への対処必要"]
WaitFree["ウェイトフリー<br/>・全プロセスの進行保証<br/>・最も強い進行保証<br/>・実装が複雑"]
end
subgraph "CAS による ロックフリースタック"
Init["初期状態<br/>Top → Node1 → Node2 → null"]
Push1["Push(NewNode)<br/>1. t = Top を読み取り"]
Push2["2. NewNode.next = t"]
Push3["3. CAS(&Top, t, NewNode)<br/>成功ならNewNodeが新しいTop"]
Pop1["Pop()<br/>1. t = Top を読み取り"]
Pop2["2. t == null なら null返却"]
Pop3["3. CAS(&Top, t, t.next)<br/>成功なら t を返却"]
Init --> Push1
Push1 --> Push2
Push2 --> Push3
Init --> Pop1
Pop1 --> Pop2
Pop2 --> Pop3
end
subgraph "ABA問題と対策"
ABA_Problem["ABA問題<br/>1. スレッドAが値Aを読み取り<br/>2. スレッドBが A→B→A に変更<br/>3. スレッドAのCASが誤って成功"]
Solution1["対策1: ポインタタグ<br/>・ポインタに世代番号付加<br/>・ABA→A'B'A''に変化"]
Solution2["対策2: ハザードポインタ<br/>・使用中ポインタを保護<br/>・ガベージコレクション延期"]
Solution3["対策3: RCU<br/>・Read-Copy-Update<br/>・読み手を妨げない更新"]
end
subgraph "進行性の保証レベル"
Obstruction["妨害自由<br/>（Obstruction-Free）<br/>単独実行なら進行"]
LockFreeGuarantee["ロックフリー<br/>（Lock-Free）<br/>システム全体で進行"]
WaitFreeGuarantee["ウェイトフリー<br/>（Wait-Free）<br/>各スレッドが進行"]
Obstruction --> LockFreeGuarantee
LockFreeGuarantee --> WaitFreeGuarantee
end
end
style LockBased fill:#ffebee
style LockFree fill:#e8f5e8
style WaitFree fill:#e3f2fd
style ABA_Problem fill:#fff3e0
style WaitFreeGuarantee fill:#f3e5f5
定義 12.10 データ構造がロックフリー⟺ 無限のステップ中で、少なくとも1つの操作が完了する。
CAS（Compare-and-Swap）：
CAS(addr, old, new):
atomically:
if *addr == old:
*addr = new
return true
else:
return false
例：ロックフリースタック
Push(x):
loop:
t = Top
x.next = t
if CAS(&Top, t, x):
return
Pop():
loop:
t = Top
if t == null:
return null
if CAS(&Top, t, t.next):
return t
12.6.3 線形化可能性
定義 12.11 並行オブジェクトが線形化可能⟺ 各操作が、呼び出しと応答の間のある時点で瞬間的に効果を持つように見える。
性質：
- 合成可能性：線形化可能なオブジェクトの組み合わせも線形化可能
- 局所性：各オブジェクトを独立に推論可能
12.7 プロセス計算の高度な話題
12.7.1 π計算
構文：
P ::= 0 | τ.P | x(y).P | x̄⟨y⟩.P | P|Q | (νx)P | !P
名前の移動性： チャネル名を値として送受信できる。
スコープ拡張：
(νx)(x̄⟨z⟩.P | Q) | x(y).R → (νx)(P | Q | R[z/y])
12.7.2 Ambient 計算
移動性のモデル化： プロセスが階層的な場所（ambient）間を移動。
基本操作：
- in n：ambient n に入る
- out n：ambient n から出る
- open n：ambient n を開く
12.7.3 確率的プロセス代数
確率的選択： P +_p Q：確率 p で P、確率 1-p で Q を選択
応用：
- 性能解析
- 信頼性評価
- ランダム化プロトコルの検証
12.8 実時間システム
12.8.1 時間オートマトン
定義 12.12 時間オートマトンは以下の組：
- 有限の場所集合
- クロック変数の有限集合
- クロック制約付き遷移
意味論：
- 時間経過：すべてのクロックが同じ速度で進む
- 離散遷移：ガード条件を満たすとき遷移、クロックリセット
12.8.2 時間付き時相論理
TCTL（Timed CTL）：
- EF_{≤d} φ：d 時間単位以内に φ となる経路が存在
- AG_{≤d} φ：すべての経路で d 時間単位まで常に φ
モデル検査： 領域グラフによる有限表現。
章末問題
基礎問題
- 2つのプロセスが交互に実行される以下のプログラムで、
最終的な x の値として可能なものをすべて求めよ：
共有変数: x = 0 P1: x = x + 1; x = x + 1 P2: x = x * 2 -
CCS で以下のプロセスの双模倣等価性を判定せよ： (a) a.b.0 + a.c.0 と a.(b.0 + c.0) (b) (a.0 | b.0){a} と b.0
-
哲学者の食事問題を Petri ネットでモデル化し、 デッドロックが起こることを示せ。
- n プロセスのベーカリーアルゴリズムが相互排除を満たすことを証明せよ。
発展問題
-
分散システムにおける論理時計について： (a) Lamport 時計の定義と性質を述べよ (b) ベクトル時計との違いを説明せよ
-
コンセンサス数について： (a) 各同期プリミティブのコンセンサス数を求めよ (b) 階層定理を説明せよ
-
ロックフリーキューの実装： (a) Michael-Scott アルゴリズムを説明せよ (b) ABA 問題とその対策を論ぜよ
-
弱メモリモデルについて： (a) TSO と PSO の違いを説明せよ (b) メモリバリアの必要性を例を挙げて示せ
探究課題
-
ブロックチェーンのコンセンサスアルゴリズムについて調査し、 Proof of Work、Proof of Stake、PBFT の特徴を比較せよ。
-
トランザクショナルメモリについて調査し、 ソフトウェア実装とハードウェア実装の得失を論ぜよ。
-
アクターモデルについて調査し、 共有メモリモデルとの違いと実装例（Erlang、Akka）を説明せよ。
-
形式的検証ツール（TLA+、SPIN、NuSMV など）について調査し、 産業界での応用例を示せ。