並列・分散アルゴリズムの基礎
7/30 マルレク「並列・分散アルゴリズムの基礎」へのお誘い
7月30日、「並列・分散アルゴリズムの基礎」をテーマにマルレクを開催します。https://concurrent.peatix.com/view
今回のセミナーには、大きく二つの目的があります。
第一は、「排他制御 Mutual Exclusion 」「生産者・消費者同期 Producer-Consumer Synchronization 」といった基本的な並列アルゴリズムを、改めて学ぶことです。
これらのアルゴリズムは、1960年代の半ばにダイクストラらによって定式化されたもので、計算科学のいわば「古典」と言ってもいいものです。
ただ、こうした知識が、現代では不要になったわけではありません。
セミナーの第二の目的は、こうした並列・分散アルゴリズムの基礎理論が、現代ではどのように捉え返され新しい理論化がなされているのか、その一端を紹介することです。
基本的には、並列・分散アルゴリズムのSafety Property（間違った処理を行わないこと）、Liveness Property(ある処理が行われるべきこと)、Fairness（Liveness Property の緻密化）といった概念を紹介したいと思っています。
Liveness / Fairness は、直接はdeadlock の回避と理解されてもいいのですが、livelockやunfairなリソース配分や、このところ話題の「輻輳」が起きないことを含んだ広い概念です。
今回のセミナーの骨組みは、2015年のランポートのTuring賞受賞講演に全面的に依拠しています。興味がある方は、是非、原論文をお読みください。
"The Computer Science of Concurrency: The Early Years"
https://cacm.acm.org/magazines/2015/6/187316-turing-lecture-the-computer-science-of-concurrency/fulltext#R9
お申し込みは、こちらからお願いします。
https://concurrent.peatix.com/view
講演資料 「並列・分散アルゴリズムの基礎」（ダウンロード）
セミナー解説blog
- あのころみんな若かった
- go to 文も素晴らしい！
- これは、やさしいアルゴリズムだ!
- アルゴリズムを図解する
- 無理は承知で …
- 次章へ。その前に ...
- なぜ、歴史を振り返るのか？
- アルゴリズムとプログラムは違うものです
- アルゴリズムの振る舞いを図解する
- アルゴリズムの不変量
- 相対論とプログラミング
- アルゴリズムの標準モデル
セミナー解説資料
排他制御 1 ダイクストラ
ダイクストラのMutual Exclusion アルゴリズム 1
( スライドのpdf blog:「あのころみんな若かった」)
ダイクストラのMutual Exclusion アルゴリズム 詳細
( スライドのpdf blog:「go to 文も素晴らしい！」)
排他制御 2 ランポート
ランポートのbakeryアルゴリズム 1
( スライドのpdf blog:「これは、やさしいアルゴリズムだ！」)
ランポートのbakeryアルゴリズムの正しさ
( スライドのpdf blog:「アルゴリズムを図解する」)
新しいbakeryアルゴリズムと並列性の表現
生産者消費者同期
ダイクストラのsemaphore
( スライドのpdf blog:「次章へ。その前に ...」)
生産者消費者同期アルゴリズムを記述する
( スライドのpdf blog:「なぜ、歴史を振り返るのか？」)
Producer-Consumerアルゴリズムの振る舞いを図解する
( スライドのpdf blog:「アルゴリズムの振る舞いを図解する」)
アルゴリズムの正しさへのアプローチ
アルゴリズムとプログラム
( スライドのpdf blog:「アルゴリズムとプログラムは違うものです」)
状態モデルとアルゴリズムの「不変量」
( スライドのpdf blog:「アルゴリズムの不変量」)
イベントの順序関係とランポートの「論理的時計」
( スライドのpdf blog:「相対論とプログラミング」)
状態とアクションと時制論理式
( スライドのpdf blog:「アルゴリズムの標準モデル」)
MaruLabo 関連ページ
「プログラムと論理」 2019/10/10 マルゼミ
小論は、 Deep Specificationのような現代の「形式的手法」の理解を深めることを目的としている。
現代の「形式的手法」には、いずれも50年近く前の1970年代に遡る、二つの異なった「起源」がある。両者ともに「プログラムと論理」という問題意識は共通していたのだが、生まれた場所が異なっていた。一つは、論理学＝数学の領域で生まれ、もう一つは計算機科学の領域で生まれた。
前者の代表は、ハワードやマーチン・レフである。彼らは、「型の理論」を作り上げ、抽象的だが、プログラムの実行は、ある定理の証明に他ならないという認識にたどり着いた。
後者の代表は、ホーアやダイクストラである。彼らは、代入文やif文、シーケンシャルな実行や繰り返しのWhile文といった具体的なプログラムの構成と論理との関係を研究した。
ただ、 20世紀の段階では、 「プログラムと論理」という問題を扱うには、 論理学＝数学からのアプローチでは、現実のコンピュータ技術や具体的なプログラム言語との接点は明確ではなかった。計算機科学からのアプローチでは、論理の多様な性質への理解と、何よりも強力な「証明マシン」を欠いていた。
様々な紆余曲折を経て、両者の統一は、21世紀に持ち込まれることとなった。筆者は、こうした二つの流れが合流したところに、 Deep Specificationのような現代の「形式的手法」が生まれたと捉えている。
小論では、20世紀に計算機科学の中で追求された「形式的手法」とその「挫折」を、一つのトピックにしている。このテーマでは、歴史を振り返るのには意味があると考えている。なぜなら、現代の「形式的手法」は、かつて一度失敗したムーブメントの再復活という面を持つからである。
現代の形式的手法の紹介は、前回のマルレクに続くものだが、今回は、出来るだけ具体的な実例の紹介を心がけた。
コンピュータが論理的＝数学的推論能力を持つことの認識と強力な証明マシンの存在こそが、20世紀の形式的手法と現代の形式的手法を分かつ最大の違いだと筆者は考えている。
と言っても、講演とスライドだけでは、「コンピュータによる証明」「コンピュータによる証明のチェック」の強力さ（スピードと規模感）が伝わらないと感じている。その技術は、現代の我々の手の届くところにあるのだ。ただ、多くのIT技術者は、そのことに気づいていない。
改めて、現代の形式的手法の基礎であり、現代のソフトウェア科学の Lingua Franca であるCoqの利用者を増やすことの重要性を強く感じている。
「分散合意アルゴリズム -- Paxos」 2022/01/29 マルレク
今回のマルレクのテーマは、代表的な「分散合意アルゴリズム」であるPaxosの紹介です。
なんで今頃Paxosなのかと感じる人もいると思います。IT系の話題を取り上げるのは久しぶりなので、最初に、このセミナーの背景を述べておこうと思います。それは、現在の日本で、大規模なシステム障害が連続して起きていることと、すこし関係しています。
21世紀初頭のIT技術とITビジネスの大きな変化は、膨大な計算資源を集中してネットワークを通じてサービスを提供するクラウドと呼ばれる巨大なシステムの成立によって特徴づけられます。こうしたクラウドへのリソースの集中に対応して、クラウドのサービスを利用するクラウド・デバイスとしてのスマートフォンが拡散し、ほとんど全人類に普及します。
技術者のライフサイクルからみれば、このクラウド時代への移行は、驚くほど短期間に急速に進行しました。
大規模システムというのは、単に、システムの規模が大きいことを意味しません。今日では、大規模システムは、設計者がそれを意識するか否かに関わらず、クラウドと同じようにネットワークをまたいだ大規模分散システムの形を取ります。
プログラミングのスタイルも大きく変わりました。サーバーサイドでサービスを作るプログラマも、クライアントサイドでアプリを作るプログラマも、本人がそれを意識すると否とに関わらず、今日のプログラマの大部分は、ネットワーク・プログラマです。
クラウド技術はもちろんネットワーク技術なのですが、クラウド技術成立の前提には、「ネットワーク上で規模を拡大しながら、システム全体としては障害を起こさないシステムを作ることは難しい」という認識があったことです。この認識は「ハードウェアの障害は起きるものだ」という障害観の成立とともに、重要なものだと思います。
クラウドの技術は、まさにこうした困難を乗り越える技術として登場しました。また、それは、冒頭でも見たように、大きな成功を収めました。
ただ、僕は、変化のスピードが早すぎて --- 繰り返しますが、技術者のライフサイクルから見ればということですが --- ネットワーク上でシステムを構築するというクラウド時代の中心的変化の技術的な意味が、クラウド以前の技術者にもクラウド以降の技術者にも、きちんと伝わっていないのではという心配をもっています。
それは、クラウド以前の技術者だけの問題ではありません。若い技術者は、必ずしもクラウド技術の一時代を画したGoogleの"Google File System (GFS)" や"BigTable" に関心を持っているわけではないように思えます。
GFSとBigTableは、直接的には異なる目的のために開発されたものです。ただ、両者で共通に利用されている "Chubby"と呼ばれた「分散ロック・サービス」は、Paxosの実装にほかなりません。見かけは地味ですが、こうした形での「分散合意アルゴリズム」の利用には、クラウド技術のエッセンスが詰まっていると僕は考えています。
10年以上前の技術の昔話をするつもりはありません。「風が吹けばオケ屋が儲かる」式に「Paxosがわかればクラウド技術がわかる」という話をするつもりもありません。ただ、知らないままに通り過ぎる訳にはいかない技術は存在します。
その上、「分散合意」技術、けっして完成した過去の枯れた技術ではありません。その重要性は、現代のIT技術においても、新しい装いのもとに引きつがれています。
