第12章並行計算の理論

章プロフィール

並列・分散システムの理論的基礎

読了目安 3〜4週間

難易度 ★★★★

章構成 6節

主要トピック

並行計算モデル
プロセス代数
Petri ネット
時相論理による検証
分散アルゴリズム
並行データ構造

戻り先

付録A: 記法付録C: 解答付録D: 用語付録F: 進捗

はじめに

並行計算の理論は、複数の計算プロセスが同時に実行される状況を数学的に扱う分野です。マルチコアプロセッサ、分散システム、クラウドコンピューティングの普及により、並行性の理解と制御は現代のコンピュータサイエンスにおいて不可欠となっています。本章では、並行システムのモデル化、解析、検証のための理論的基礎を体系的に学びます。

並行性がもたらす非決定性、デッドロック、競合状態などの問題は、逐次プログラムでは現れない固有の複雑さを持ちます。これらの問題を理解し、解決するための形式的手法は、信頼性の高い並行システムの設計に欠かせません。本章で学ぶ理論は、オペレーティングシステム、データベース、分散アルゴリズムなど、幅広い分野の基礎となります。

通し例: 安全なメッセージ配送基盤 複数ワーカーが配送キューを同時更新し、複数ノードが順序付きログを複製する状況では、競合・整合性・合意が一度に問題になります。本章では、通し例を並行・分散システムとして読み替え、正当性と不可能性を同時に扱います。

学習目標

並行計算のモデル（共有メモリ/メッセージパッシング）を説明できる
双模倣等価や形式モデル（CCS/π計算、LTS）の基礎を説明できる
Petri ネットの基本構成と到達可能性などの性質を説明できる
合意問題や FLP 不可能性、線形化可能性・順序整合性の概念を概説できる
ロックフリー・wait-free の直観とデータ構造設計の要点を説明できる

12.1 並行計算モデル

12.1.1 並行性の基本概念

並行計算の基本概念

定義 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）

背景：共有メモリモデルは、同じデータ構造を複数スレッドで扱う場面を抽象化したものです。逐次プログラムでは自明だった「いつ書き込みが見えるか」「読み書きがどこで衝突するか」を、明示的に考える必要があります。

最小例：

共有変数: x = 0

P1: r1 = x; x = r1 + 1
P2: r2 = x; x = r2 + 1

逐次実行なら最終的に x = 2 ですが、2つの読取りが先に走ると x = 1 で終了します。これは競合状態による「更新の取りこぼし」の最小例です。

注意点：原子的な read-modify-write を使っても、複数変数の公開順序まで自動的に保証されるとは限りません。原子性と可視性は別の論点として切り分けて考えます。

【実務メモ：メモリモデルの落とし穴】

可視性: 他スレッドへの書き込みが即座に観測されるとは限らない。共有変数の出版には適切なフェンス/アトミック（acquire/release）を用いる。
再順序化: コンパイラ/CPU最適化により命令順が入れ替わる。happens-before の関係を明示できる同期原語を使う。
データ競合: 同一位置への競合アクセス（うち1つ以上が書き込み）は未定義挙動/未規定結果。アトミック/ロックで防止。

【happens-before 簡易ガイド】

取得（acquire）と解放（release）で順序を確立：release 前の書込みは、対応する acquire 後の読み手に可視。
共有変数の公開は store-release、読取りは load-acquire を基本に（言語/ライブラリの原語に従う）。
データ構造の公開時は構築完了→release→参照配布→acquire→使用、の順を守る。

直観図：happens-before（HB）関係のタイムライン

HB 関係のタイムライン

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

定義 12.3 メッセージパッシングシステムでは、プロセスがメッセージ送受信により通信する。

通信プリミティブ：

send(p, m)：プロセス p にメッセージ m を送信
receive(q)：プロセス q からメッセージを受信

同期性：

同期通信：送信と受信が同時に起こる
非同期通信：送信後、受信まで遅延がある

背景：メッセージパッシングモデルでは、共有変数そのものではなく「誰が誰に何を送ったか」を直接議論します。通信遅延や故障をモデルに組み込みやすいため、分散システムやアクターモデルで広く用いられます。

最小例：

Client: send(Server, ("square", 5))
        receive(Server) = 25

Server: ("square", n) = receive(Client)
        send(Client, n * n)

同期通信なら送受信は同時に成立し、非同期通信なら送信済みメッセージがキューに蓄積されて後で受信されます。

注意点：送信順と受信順が一致するか、メッセージ喪失を許すか、再送を許すかはモデルごとに異なります。証明や設計では、チャネルの性質を先に固定します。

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, …：入力アクション
\(\overline{a}, \overline{b}, \overline{c}, \ldots\)：出力アクション
τ：内部アクション

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^{\prime}\) ⇒ ∃\(Q^{\prime}\), Q –α–> \(Q^{\prime}\) かつ \(P^{\prime}\,R\,Q^{\prime}\)
Q –α–> \(Q^{\prime}\) ⇒ ∃\(P^{\prime}\), P –α–> \(P^{\prime}\) かつ \(P^{\prime}\,R\,Q^{\prime}\)

定義 12.6 \(P\) と \(Q\) が双模倣等価（\(P \sim Q\)）\(\Leftrightarrow\) ある双模倣 \(R\) で \(P\,R\,Q\)

背景：双模倣等価は、単に同じアクション列を実行できるかではなく、途中状態でも相手の振る舞いを追い続けられるかを比較します。そのため、トレース等価よりも分岐構造に敏感です。

最小例： P = a.0 + a.0 と Q = a.0 は、どちらも a を1回実行すると停止するため双模倣等価です。一方、a.b.0 + a.c.0 と a.(b.0 + c.0) では、後者だけが a の後に b と c の両方を選べるため、双模倣等価ではありません。

注意点：分岐の位置が1ステップずれるだけでも等価性は崩れます。反例を探すときは、「片方だけが次に実行できるアクション」を見つけると整理しやすくなります。

定理 12.1 双模倣等価性は合同関係である（すべての文脈で保存される）。

12.2.4 その他のプロセス代数

CSP（Communicating Sequential Processes）：

失敗意味論
トレース、失敗、発散

π計算：

名前の移動性
チャネルを値として送受信可能

12.3 Petri ネット

12.3.1 基本定義

Petriネットによる並行システムモデリング

定義 12.7 Petri ネットは5つ組 \(N = (P, T, F, W, M_0)\)：

P：プレース（場所）の有限集合
T：トランジション（遷移）の有限集合（\(P \cap T = \emptyset\)）
\(F \subseteq (P \times T) \cup (T \times P)\)：フロー関係
\(W: F \to \mathbb{N}_{>0}\)：重み関数
\(M_0: P \to \mathbb{N}\)：初期マーキング

12.3.2 実行意味論

定義 12.8 トランジション \(t\) が発火可能 \(\Leftrightarrow\)

\(∀p ∈ •t, M(p) ≥ W(p, t)\)

発火規則：t が発火すると、マーキングは以下のように変化：

\(∀p ∈ •t: M^{\prime}(p) = M(p) - W(p, t)\)
\(∀p ∈ t•: M^{\prime}(p) = M(p) + W(t, p)\)
その他：\(M^{\prime}(p) = M(p)\)

背景： Petri ネットでは、トークンが「現在どの資源や条件が有効か」を表します。複数のトランジションが同時に発火可能になりうるため、逐次的な状態遷移図より自然に並行性を表現できます。

最小例：プレース idle に1個、busy に0個のトークンを置き、トランジション start を idle -> busy とします。 start は idle にトークンがあるときだけ発火でき、発火後は idle = 0, busy = 1 となります。

注意点：状態方程式を満たしても、本当にそのマーキングへ到達できるとは限りません。到達可能性を論じるときは、可達木や不変量と併用します。

12.3.3 性質解析

到達可能性：初期マーキング \(M_0\) から到達可能なマーキングの集合 \(R(N, M_0)\)。

構造的性質：

有界性：\(\forall M \in R(N, M_0),\ \forall p \in P,\ M(p) \le k\)
安全性：1-有界性
活性：すべての到達可能マーキングから各トランジションが発火可能

不変量：

P-不変量：Y^T · C = 0 を満たすベクトル Y
T-不変量：C · X = 0 を満たすベクトル X

（C は接続行列）

12.3.4 解析手法

可達木：到達可能なマーキングを木構造で表現。無限の場合は ω を使用。

線形代数的手法：状態方程式：\(M = M_0 + C \cdot \sigma\)（\(\sigma\) は発火回数ベクトル）

定理 12.2 M が到達可能ならば状態方程式を満たす（逆は一般に不成立）。

12.4 時相論理による並行システムの検証

12.4.1 並行システムの性質

安全性（Safety）：「悪いことは起こらない」

相互排除：同時にクリティカルセクションに入らない
部分正当性：終了すれば正しい結果

活性（Liveness）：「良いことがいつか起こる」

無飢餓性：要求したプロセスはいつかリソースを得る
全域的進行：システム全体が進行する

公平性（Fairness）：

弱公平性：永続的に可能な動作はいつか実行される
強公平性：無限回可能な動作はいつか実行される

12.4.2 CTL による検証

並行システムのモデル化： Kripke 構造 \(M = (S, S_0, R, L)\)

S：状態集合
\(S_0\)：初期状態集合
R：遷移関係
L：ラベリング関数

典型的な性質の記述：

相互排除：\(AG\ \lnot (\mathrm{critical}_1 \land \mathrm{critical}_2)\)
応答性：AG (request → AF grant)
無飢餓：AG (request → AF critical)

背景： CTL では、「すべての経路で成り立つか」（A）と「ある経路で成り立つか」（E）を明示します。分岐を含むシステムに対して、到達可能性と安全性を同じ論理で記述できる点が利点です。

最小例： 3状態 idle, p1_cs, p2_cs からなる相互排除モデルを考えます。どの状態でも critical_1 と critical_2 が同時に真でないなら AG ¬(critical_1 ∧ critical_2) が成立し、 request_1 が立った後に必ず p1_cs へ進めるなら AG (request_1 → AF critical_1) が無飢餓性を表します。

注意点： AF φ は「どこかの経路でいつか φ」ではなく、「すべての経路で最終的に φ」を意味します。A/E と F/G の読み違いは初学者がつまずきやすい点です。

12.4.3 モデル検査アルゴリズム

状態爆発問題：プロセス数に対して状態数が指数的に増加。

対策：

シンボリックモデル検査（BDD を使用）
有界モデル検査（SAT ソルバを使用）
抽象化技法

直観図：Coffman の4条件と資源割当グラフ（デッドロック例）

デッドロックのCoffmanの4条件

【実務メモ：デッドロックと活性阻害】

デッドロック（Coffman の4条件）: 相互排他・占有待ち・非奪取・循環待ち。
- 回避策: 一貫したロック順序、try-lock + バックオフ、タイムアウト/取り消し、資源階層化、デッドロック検出。
優先度逆転/飢餓: 高優先度タスクが低優先度にブロックされる。優先度継承/天井プロトコル、フェアロック等を検討。

12.4.4 最小実行例（TLA+ / TLC）

ここでは、2プロセス相互排除（Peterson）を有限状態でモデル化し、安全性（相互排除）をモデル検査で確認する最小例を示します。

例ファイル： Peterson.tla, Peterson.cfg
必要要件：TLC（TLA+ Toolbox または tla2tools.jar）、（CLI実行する場合は）Java

# tla2tools.jar を用いるCLI実行例（jarの入手/配置は環境に依存）
cd docs/assets/examples/formal-methods/tla
java -cp tla2tools.jar tlc2.TLC -config Peterson.cfg Peterson.tla

注：モデル検査の基本概念（性質の書き方、状態爆発と対策）は第9章も参照してください。

12.5 分散アルゴリズム

12.5.1 分散システムのモデル

システムモデル：

プロセス故障：クラッシュ、ビザンチン
通信：同期、非同期
ネットワーク：完全グラフ、任意トポロジー

複雑性尺度：

メッセージ複雑度
時間複雑度（ラウンド数）
空間複雑度（局所）

12.5.2 基本的な分散アルゴリズム

リーダー選出

LCR アルゴリズム（リング上）：

各プロセス p：
1. 自分の ID を右隣に送信
2. 受信した ID が自分より大きければ転送
3. 自分の ID を受信したらリーダー

メッセージ複雑度：O(n^2)
時間複雑度：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

最小例： 2プロセス P0, P1 が同時に入場要求し、 P0 が札 1、P1 が札 2 を取ったとします。辞書式順序 (number, pid) により P0 が先に入り、 P1 は P0 が number[0] = 0 に戻すまで待機します。

注意点：この議論は、故障しない共有メモリ環境を前提としています。分散環境やクラッシュ故障を扱う場合は、時計同期やメッセージ交換に基づく別の相互排除法が必要です。

12.5.3 合意問題

定義 12.9 合意問題の要件：

合意：すべての正常プロセスは同じ値を出力
妥当性：出力値は入力値の一つ
停止性：正常プロセスは有限時間で出力

背景：合意問題は、複数プロセスが1つの値に収束できるかを問う基本問題です。複製ログ、分散トランザクション、ブロックチェーンなど、多くの実システムはこの抽象問題として整理できます。

最小例： 3プロセスがそれぞれ 0, 1, 1 を提案するとします。全員が 1 を出力すれば合意と妥当性を満たしますが、1台でも 0 を出力すると合意に失敗します。

注意点：合意の可否は、同期仮定と故障モデルに強く依存します。n > 3f や FLP の結論は、前提を変えるとそのまま適用できません。

Byzantine 将軍問題

定理 12.3 n 個のプロセスのうち f 個が Byzantine 故障の場合、

合意が可能 \(\Leftrightarrow\) \(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 ロックフリーアルゴリズム

並行データ構造の設計手法

定義 12.10 データ構造がロックフリー \(\Leftrightarrow\)

無限のステップ中で、少なくとも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

最小例： Top = A のスタックで Push(B) と Pop() が競合すると、どちらか一方の CAS が失敗して再試行します。それでも少なくとも一方の操作は前進するため、この振る舞いがロックフリー性の直観になります。

直観図：ABA問題の概念図と緩和策の示唆

ABA問題の概念図

【実務メモ：ロックフリー/wait-free の注意】

ロックフリー: どこかのスレッドが常に前進する。wait-free: 全スレッドが有限ステップで完了する。
典型的落とし穴: ABA 問題（CAS で同一値に見える）、安全なメモリ解放（Hazard Pointers や Epoch ベースの再生手法）、偽共有（false sharing）。
アトミック操作のメモリ順序は明示する（seq_cst, acq_rel, relaxed など）。必要最小限の順序を選び、性能と正しさを両立させる。

12.6.3 線形化可能性

定義 12.11 並行オブジェクトが線形化可能 \(\Leftrightarrow\)

各操作が、呼び出しと応答の間のある時点で瞬間的に効果を持つように見える。

背景：逐次仕様で理解してきたキューやスタックを並行環境へ持ち込むとき、各操作をどの瞬間に「効いた」とみなせるかを与えるのが線形化可能性です。並行実装を逐次仕様へ還元して考えるための基本概念です。

最小例：空キューに対して enqueue(1) と dequeue() が重なって実行され、dequeue() が 1 を返したとします。この履歴は「まず enqueue(1) が効き、その直後に dequeue() が効いた」と並べ替えられるので、線形化可能とみなせます。

注意点：戻り値がもっともらしく見えても、重なった操作列を逐次履歴へ落とせなければ線形化可能とは言えません。検証では返り値だけでなく、呼出し時刻と応答時刻も追跡します。

性質：

合成可能性：線形化可能なオブジェクトの組み合わせも線形化可能
局所性：各オブジェクトを独立に推論可能

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 時間単位まで常に φ

モデル検査：領域グラフによる有限表現。

まとめ

並行性は正当性仕様（安全性・活性）と実行モデル理解が鍵
不可能性・下界・整合性モデルを理解して実装上のトレードオフを設計
検証手法（モデル検査・定理証明）を適用して品質を担保

学習を広げる補助資料

補助資料を併用するなら、理論の使われ方は付録E の第12章節、理解確認は付録F の第12章節を参照してください。

参考文献と次の一歩

図版の再参照: 本章の図をまとめて見返したいときは付録H: 図版ガイドと図一覧を参照してください。
標準: Nancy A. Lynch, 『Distributed Algorithms』. 分散アルゴリズム、不可能性、正当性証明の標準的な参照先です。
並列実装: Maurice Herlihy, Nir Shavit, 『The Art of Multiprocessor Programming』. 共有メモリ並行性と lock-free / wait-free の設計感覚を補えます。
検証: Christel Baier, Joost-Pieter Katoen, 『Principles of Model Checking』. 状態遷移系とモデル検査の側面を深めたい読者向けです。
過程代数: Robin Milner, 『Communication and Concurrency』. CCS 系の見方を原典に近い形で確認できます。
出典メモ: Lamport の論理時計、Fischer–Lynch–Paterson の不可能性結果は、本章の分散・並行計算の見取り図を支える古典です。モデルによって何が可能で何が不可能かを切り分ける姿勢が重要です。
次の一歩: 仕様記述と検証の言葉へ戻るなら第9章、実世界の応用像や学習計画へ接続したいなら付録E と付録F を参照してください。
章末問題
代表演習と詳細解答は付録C（第12章）を参照。

取り組み方ガイド

迷ったら次の表の順で進め、詰まったら「主に戻る節」にある実行モデル・安全性条件・典型アルゴリズムを先に見直してください。

区分	推奨順	主に戻る節	使い方
基礎問題	1番目	12.1〜12.4	モデル化と正当性条件の基本を確認する
発展問題	2番目	12.4〜12.6	合意・進行保証・弱メモリの差分を詰める
探究課題	3番目	12.1〜12.6	実システムへの適用と制約を比較する

基礎問題

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 など）について調査し、産業界での応用例を示せ。

第12章 並行計算の理論