並列・分散アルゴリズムの基礎

全体概要

本セミナー「並列・分散アルゴリズムの基礎」は、並列・分散プログラミングにおける根本的な問いを探求します。その問いとは「複数の独立したプロセスが、共有リソースへの排他的アクセスやデータの受け渡しを、正しく・安全に・効率的に実現するにはどうすればよいか」というものです。

出発点となるのは1965年のダイクストラによる歴史的論文 "Solution of a Problem in Concurrent Programming Control" です [p.8]。当時すでに3年以上未解決だったこの問題は、複数のコンピュータが共有メモリを通じてのみ通信できる環境で、「クリティカルセクション」への排他的アクセスをどう保証するかというものでした。ダイクストラはこの問題を初めて厳密に定式化し、解法を与えました。

1974年にランポートは、ダイクストラの解法が持つ「下位レベルの排他制御に依存する」という根本的欠陥を克服する "bakeryアルゴリズム" を発表します [p.56]。パン屋の整理券という直感的なメタファーに基づくこのアルゴリズムは、アトミックな共有メモリ操作を一切前提とせずに排他制御を実現した、分散アルゴリズム史上の金字塔です。

さらにセミナーは生産者消費者同期問題へと進み、ダイクストラのセマフォ概念とその活用法 [p.112]、そしてランポートのPlusCal記述言語による形式的アルゴリズム記述 [p.124] を丁寧に解説します。

最後に、アルゴリズムの「正しさ」を論じるための理論的基盤として、状態モデルと不変量 [p.161]、分散システムにおける論理的時計 [p.170]、そしてアクションの時制論理（TLA） [p.190] という三つのアプローチが体系的に提示されます。本セミナーは、実装技術を超えた「アルゴリズムとは何か」「正しさとは何か」という深い問いに対し、1960年代から1990年代にわたる知的遺産を縦断して答えようとする、密度の高い講義です。

講義のロードマップ

■ Part I: 排他制御 ダイクストラ

• この部の核心:

「どうすれば複数の独立したプロセスが、同時に一つだけクリティカルセクションを実行することを保証できるか」というダイクストラの問いを出発点に、その問題の意味、解の条件、具体的アルゴリズム、そして証明の構造を順に追います。この問題が1962年以来未解決であったこと、そしてその解の重要性をダイクストラ自身が強調していた事実が印象的です [p.9]。

• 論理展開:
• 問題の定式化: N台のコンピュータが共有メモリ（`integer k`, `boolean b[1:N]`, `boolean c[1:N]`）を通じてのみ通信し、排他的クリティカルセクション実行を実現する。解は「対称性・速度非依存・非クリティカルセクションでの停止許容・デッドロックフリー」を満たさなければならない [p.16], [p.17]。
• アルゴリズムの構造: `k=i` を満たすプロセスのみがクリティカルセクションへの接近権を得る。Li4ブロックで自分以外の全 `c[j]` が真であることを確認して初めてクリティカルセクションに入る [p.27], [p.32]。
• 証明の二本柱: ①二つのプロセスが同時にクリティカルセクションに入らない（safety）、②「お先にどうぞ」のデッドロックが起きない（liveness）の二点をそれぞれ論証する [p.30], [p.36]。
• 留意点: このアルゴリズムには後続研究者による改善の余地があることが予告されている [p.23]。

■ Part II: 排他制御 ランポート

• この部の核心:

ダイクストラのアルゴリズムが「共有変数へのアトミックな読み書き」という下位レベルの排他制御に依存するという根本的問題を指摘し、ランポートのbakeryアルゴリズムがその制約を取り除く革命的解法であることを示します [p.54]。1973年当時「不可能」とされていた「下位の排他制御を前提としない排他制御」の最初の実装です [p.86]。

• 論理展開:
• bakeryアルゴリズムの仕組み: 各プロセスはチケット番号 `number[i] := 1 + maximum(number[1],...,number[N])` を選択し、`choosing` フラグで選択中を通知。全プロセスの番号チェック後、最小番号（同値時はプロセスIDで決定）のプロセスがクリティカルセクションへ [p.57]。
• 正しさの三つの主張: 主張1「先入店者は番号が小さい」[p.73]、主張2「クリティカルセクション入場者の番号は最小」（safety）[p.75]、主張3「レジ待ちのプロセスはいずれ入場できる」（liveness）[p.82]。
• 驚くべき性質: コンカレントな書き込み中に異常値を読んでも正しく動作する。チケット番号のアトミックな読み書きが不要 [p.85]。
• 新しいbakeryアルゴリズムとforall並列記法: 1979年版では `for all j do wait until ... od` という並列実行構文が導入され、並列性の表現が洗練される [p.90], [p.94]。

■ Part III: 生産者消費者同期

• この部の核心:

バッファを介した生産者・消費者間の同期問題を、ダイクストラのセマフォを用いた古典的定式化から、ランポートのPlusCal記述言語による形式的仕様記述まで、二段階で提示します。問題の本質は「バッファフルでの待機」と「バッファ空での待機」という双方向の同期制約です [p.111]。

• 論理展開:
• セマフォの定義: `V(S)`（値を1増やす）と `P(S)`（値を1減らす、0なら待機）はアトミック操作。通常の `S=S+1` とは異なり競合状態が発生しない [p.112], [p.113]。
• ダイクストラの記述: `number of queuing portions` セマフォを用い、生産者が `V`、消費者が `P` を呼ぶ古典的アルゴリズム [p.120]。
• ランポートの記述: `await Len(buf) 0` を条件とするfairプロセスとして定式化。Sequences Moduleの `Head`、`Tail`、`Append` 演算子でFIFO操作を表現 [p.124], [p.130]。
• 振る舞いの図解: バッファ容量 `LB` の増減として状態遷移を可視化。`LB=N` でProducer待機、`LB=0` でConsumer待機という境界条件が対称的に現れる [p.149], [p.150]。

■ Part IV: アルゴリズムの正しさへのアプローチ

• この部の核心:

「プログラム」と「アルゴリズム」は異なるものであり、アルゴリズムはプログラムの「意味」としての抽象的仕様であるという認識を出発点に [p.156]、アルゴリズムの正しさを論じるための三つの理論的アプローチ（不変量、論理的時計、時制論理）を体系的に提示します。

• 論理展開:
• 不変量によるアプローチ: bounded FIFO queueの不変量 `(Len(buf) ≤ N) ∧ (Input = out ∘ buf ∘ in)` が全状態遷移を通じて保持されることを帰納法で示す。この不変式の存在がアルゴリズムの仕様としての正しさを担保する [p.166], [p.167]。
• 論理的時計によるアプローチ: ランポートの1978年論文に基づき、「先に起きる（`a → b`）」関係を物理時計なしで定義。同一プロセス内の順序とメッセージ送受信から半順序を導出し、タイムスタンプによって全順序に拡張する分散アルゴリズムを提示 [p.177], [p.185]。
• 時制論理によるアプローチ: TLA（Temporal Logic of Actions）では、アクションを「状態のペアについての述語」として定義し `[[A]](s,t)` で表現。`□`（always）と `◇`（eventually）演算子、不変則 `{P}A{P} / □[A] ⇒ (P ⇒ □P)`、プログラム全体を `Π ≜ Init_Π ∧ □[N_Π] ∧ L_Π` として時制論理式で記述する枠組みを提示 [p.191], [p.193], [p.201], [p.202]。