講演資料
講義資料スライドの表紙です。上のスライド画像をクリックすると、同じ画面のまま全編のPDF資料を快適に閲覧・印刷することができます。
セミナーの概要
本セミナー「並列・分散アルゴリズムの基礎」は、並列・分散プログラミングにおける根本的な問いを探求します。その問いとは「複数の独立したプロセスが、共有リソースへの排他的アクセスやデータの受け渡しを、正しく・安全に・効率的に実現するにはどうすればよいか」というものです。
出発点となるのは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]。
■ Part II: 排他制御 ランポート
ダイクストラのアルゴリズムが「共有変数へのアトミックな読み書き」という下位レベルの排他制御に依存するという根本的問題を指摘し、ランポートのbakeryアルゴリズムがその制約を取り除く革命的解法であることを示します [p.54]。1973年当時「不可能」とされていた「下位の排他制御を前提としない排他制御」の最初の実装です [p.86]。
■ Part III: 生産者消費者同期
バッファを介した生産者・消費者間の同期問題を、ダイクストラのセマフォを用いた古典的定式化から、ランポートのPlusCal記述言語による形式的仕様記述まで、二段階で提示します。問題の本質は「バッファフルでの待機」と「バッファ空での待機」という双方向の同期制約です [p.111]。
■ Part IV: アルゴリズムの正しさへのアプローチ
「プログラム」と「アルゴリズム」は異なるものであり、アルゴリズムはプログラムの「意味」としての抽象的仕様であるという認識を出発点に [p.156]、アルゴリズムの正しさを論じるための三つの理論的アプローチ(不変量、論理的時計、時制論理)を体系的に提示します。
ページのナビゲート