エンジニアリング哲学：レスリー・ランポート、コードを書く前に考える

要点

• コードを書く前に考え、その思考を書き留める。 仕様とは、建築家の設計図にあたるソフトウェア版です。「考えなければ、間違いを犯すことが確実になる」のです。
• 時間はグローバルではなく、因果こそが実在である。 信頼できる共有時計が存在しない以上、出来事がいつ起きたかを問うのをやめ、何が何を引き起こしたかを問うことになります。
• happened-before（先行発生）と論理時計が因果を形式化する。 ランポートの半順序、そしてそれを実装するプロセスごとのカウンターは、ベクトル時計と現代の競合解決の種となりました。
• 正しさを厳密に定義し、それを証明する。 安全性と活性、Paxos による合意、ビザンチン障害耐性、そして TLA+ という仕様記述言語——これらはすべて、分散コンピューティングを言い伝えではなく数学として扱うことから生まれました。

原則

「分散システムとは、存在すら知らなかったコンピューターの障害によって、自分自身のコンピューターが使えなくなりうるシステムのことである。」 – レスリー・ランポート¹

彼は1987年に、自身の研究所の掲示板にこの一文を送りました。分散コンピューティングで最も引用される文となったのは、直感が信じることを拒む事柄に名前を与えているからです。¹ 自分のコンピューターでプログラムを動かしているつもりでも、実際にはそうではありません。あなたはそれを、存在を数え上げてもいない、時計の食い違う機械の集団にまたがって動かしているのです。そのどれか一台が、よりによって肝心な瞬間に故障しうる。頭の中で思い描けるシステムと、実際に動くシステムは別物であり、その隔たりこそが、あらゆる分散バグの棲み処なのです。

ランポートのライフワークは、その隔たりを楽観で塗りつぶすことの拒否でした。彼の信念は、並行システムと分散システムは直感で推論するにはあまりに繊細であり、だからこそ一行のコードも書く前に、紙の上で数学を用いて推論するというものです。「考えたからといって、間違いを犯さないとは限らない」と、彼は2013年にWired誌に語りました。「だが、考えなければ、間違いを犯すことは確実になる。」² その思考は書き留められなければなりません。書くことこそ、ずさんな思考が露わになる場だからです。「考えるためには、書かなければならない。書かずに考えているなら、考えているつもりになっているだけだ。」³ 建築家は一個のレンガが積まれる前に設計図を描きます。そのソフトウェア版が仕様です。ランポートはキャリアの後半を、私たちのシステムが壊れる理由はこれを省いているからだ、と論じることに費やしました。⁴

より深い洞察は、時間そのものに関わります。物理世界には、複数の機械にまたがって出来事を順序づけられるほど信頼できるグローバルな時計など存在しません。だから、何かがいつ起きたかを問うのをやめ、何が何を引き起こしたかを問い始めなければならないのです。分散計算の真の構造は、壁掛け時計ではなく因果なのです。⁵ ランポートが築いたほぼすべては、このひとつの事実を真剣に受け止めることから導かれます。そしてそれは、証拠の関門の根底に流れる信念と同じものです。望ましいと思う順序を勝手に前提にしてはならない。それを立証しなければならないのです。

背景

レスリー・ランポートは1941年2月7日、ニューヨーク市に生まれました。⁶ 1960年に MIT で数学の理学士号を、続いて1972年にブランダイス大学で数学の修士号と博士号を取得し、博士論文は偏微分方程式の特異点を扱ったものでした。⁶ 彼は計算機科学者として訓練を受けたわけではありません。数学者として訓練を受け、生涯その振る舞いをやめませんでした。彼のキャリアを特徴づけるのは、数学の基準——厳密な定義、明示された前提、テストではなく証明——を、大半が感覚頼みのプログラミングだった分野へ持ち込んだことです。

その仕事は四つの機関にまたがって行われました。1970年代の Massachusetts Computer Associates では、出来事の順序づけに関する基礎的な思考を行いました。SRI International（1977〜1985年）では、ビザンチン将軍の研究を生み出しました。Digital Equipment Corporation の Systems Research Center（1985年から、Compaq による買収を経て2001年まで）では、Paxos を書き、仕様化の仕事を始めました。2001年から2025年初頭の引退まで、彼は Microsoft Research に在籍しました。⁶ そのすべてを通じて手法は一貫していました。誰もが言い伝えとして扱っていた分散・並行コンピューティングの問題を見つけ、定理として述べられるほど厳密に定義し、そしてその定理を証明する——というものです。

業績

時間、時計、そして happened-before 関係

「Time, Clocks, and the Ordering of Events in a Distributed System（分散システムにおける時間、時計、および出来事の順序づけ）」は1978年にCommunications of the ACM誌に掲載され、計算機科学全体でも最も引用される論文のひとつです。2000年には、分散コンピューティングで最も影響力のある業績に贈られるダイクストラ賞を受賞しました。⁵⁶ その洞察は、一見ささやかなものです。分散システムには、共有された信頼できる時計が存在しないため、タイムスタンプを比べて二つの出来事を順序づけることはできません。分かるのは、ある出来事が別の出来事を引き起こしえたかどうかです。出来事 A が出来事 B より happened-before（先行発生） するのは、A と B が同じプロセス上にあり A が先である場合、あるいは A がメッセージの送信で B がその受信である場合です。これらを連鎖させると、happened-before 関係——形式化された因果——が得られます。⁵

決定的かつ直感に反する帰結は、happened-before があくまで半順序であって全順序ではない、ということです。異なるプロセス上にあり、その間にメッセージの連鎖を持たない二つの出来事は、真に並行です。どちらが先だったかという事実はそもそも存在せず、そうでないふりをするシステムは、ありもしない順序をでっち上げているのです。⁵ そこでランポートは、いまや誰もがランポート時計と呼ぶアルゴリズムを与えました。各プロセスはカウンターを持ち、あらゆる出来事ごとにそれを増やし、送出する各メッセージにその値を刻みます。受信側は、自分の値とメッセージのタイムスタンプの大きい方より1だけ大きい値へカウンターを進めます。⁷ この単純な規則は因果と整合したタイムスタンプを生み出し、ベクトル時計、バージョンベクトル、そして現代の分散データベースの競合解決機構そのものの種となりました。

この論文がアルゴリズムを超えて重要なのは、問いそのものを変えたからです。ランポート以前は、「これはいつ起きたのか？」が分散システムでも答えられるものと思われていました。ランポート以後、誠実な答えは「問いが間違っている——何が引き起こしたのかを問え」となりました。この問いの立て直しこそ、彼が分散コンピューティングを職人芸ではなく科学にしたと評される理由です。

Paxos、合意、そして複製状態機械

グローバルな時計がなく、機械が故障するなら、一群のコンピューターはいったいどうやって何かに——どのトランザクションがコミットされたか、誰がロックを保持しているか、ログの次のエントリは何か——合意できるのでしょうか。その問いが合意問題であり、ランポートの答えが Paxos、すなわちそれ以降に作られたほぼすべての障害耐性システムの中核をなすアルゴリズムです。彼はそれを複製状態機械のアプローチと組み合わせました。すべての複製が同じ状態から始まり、同じコマンド列を同じ順序で適用すれば、それらは同一であり続けます。つまり、分散システムを一貫させるという問題全体が、コマンドの順序に合意するという問題へと還元され、それこそまさに Paxos が提供するものなのです。⁶

Paxos がどのように発表されたかという顛末は、この分野で最も有名な教訓譚です。ランポートはそれを「The Part-Time Parliament（非常勤議会）」として書き上げ、Paxos という架空の古代ギリシャの島の立法手続きとしてアルゴリズムを枠づけました。議員たちには、同僚の名前を擬似ギリシャ語に音訳した名がつけられていました。⁸ この冗談は大惨事でした。査読者は彼が本気だと思わず、論文は取るに足らないものとして却下されました。彼の講演を聴いた人々は、インディ・ジョーンズめいた仕立てばかりを覚えていて、アルゴリズムは覚えていませんでした。⁸ 論文は何年も未発表のまま眠りました。Communications of the ACMの編集者がやがて1998年にACM Transactions on Computer Systems誌に掲載しましたが——それでもまだ寓話に包まれたままでした。⁸ それでも分野が無視し続けると、ランポートはついに白旗を上げ、2001年に「Paxos Made Simple（Paxos をやさしく）」を書き、ギリシャの装いを剥ぎ取って、その下にあると彼が言い張った真に単純なアルゴリズムを露わにしました。⁸ 彼が引き出した教訓は「人々は愚かだ」ではありませんでした。正しく重要なアイデアでさえ、思考を覆い隠せば失敗する——見せ方は仕事の一部であって、仕事と切り離されたものではない、ということだったのです。

ビザンチン将軍問題

1982年、ロバート・ショスタク、マーシャル・ピースとともに、ランポートは「The Byzantine Generals Problem（ビザンチン将軍問題）」を発表し、最も厄介な種類の障害を語るための言葉をこの分野に与えました。⁶ クラッシュした構成要素は、ビザンチンなそれに比べれば容易です。ビザンチンな構成要素とは、停止せずに嘘をつき、バグであれ、破損であれ、悪意であれ、異なる相手に異なる矛盾した情報を送るもののことです。論文の枠組みはこうです。各将軍が率いる軍の各部隊が、伝令を通じて単一の作戦——攻撃か撤退か——に合意しなければならない。一方で、未知の一部の将軍は裏切り者であり、合意を妨げようと積極的に動いている。ランポートは、システムが合意に到達しつつ許容できる裏切り者の数の正確な閾値を証明し、「もしノードが嘘をついたら？」という漠然とした不安を、明示された境界を持つ定理へと変えました。

その定理は、参加者の一部が敵対的であっても動き続けねばならないあらゆるシステムの知的な根であり——だからこそ、何十年も後に、ビザンチンという語がブロックチェーンの合意の中心に座っているのです。ランポートは暗号通貨を可能にしようとしたのではありません。「障害」が裏切りを含むとき、障害耐性とは何を意味するのかを、正確に定義しようとしたのです。

TLA+ と仕様化（そう、LaTeX も）

ランポートのキャリアを貫く筋は、コードを書く前に仕様化しなければならないという信念であり、TLA+ はその信念をツールへと作り込んだものです。Temporal Logic of Actions（時相論理） は、システムが何をすべきか——その状態、状態間の遷移、そして常に満たすべき性質（安全性：悪いことは決して起きない）と最終的に達成すべき性質（活性：良いことがいずれ起きる）——を厳密に数学的に記述するための言語です。この二つの概念も彼が形式化しました。⁶ 仕様を書くと、モデル検査器が状態空間を探索し、不変条件を破る微妙な交錯を見つけ出します——テストでは決して見つからなかったバグ、なぜなら三台の機械が、あなたが想像もしなかった順序で三つのことをしたときにしか現れないからです。彼の主張は建築家の設計図です。コンクリートを流し込む前に建物を描く。ソフトウェアの仕様も同じ設計図であり、数学は私たちが持つ最も厳密な言語だからこそ、数学で書かれるのです。⁴

そして、もうひとつの静かな金字塔があります。1980年代初頭、ドナルド・クヌースの TeX を土台に、ランポートは LaTeX を書きました——科学者と数学者が文書を組版する際の標準となったマクロシステムであり、ある世代の論文や学位論文があの見た目をしている理由です。⁶ それはランポートらしい所産です。自分の仕事を厳密に書く必要があったから、誰もがそれをできるツールを作ったのです。TLA+ を生んだ本能——厳密さを強いる記法——は、LaTeX を生んだ本能と同じものなのです。

手法

その手法は、五十年にわたり執拗に適用されたひとつの考えです。思考こそが仕事であり、思考はコードより前に書き留められなければならない。

時間ではなく因果について推論せよ。 信頼できるグローバルな時計は存在しないのだから、出来事をいつ起きたかで順序づけるのをやめ、何が何を引き起こしたかで順序づけよ。真の構造は壁掛け時計ではなく happened-before 関係であり——二つの出来事が真に並行だと受け入れるほうが、順序をでっち上げるより誠実なのです。⁵

コードを書く前に仕様化せよ。 確立された解のないものについては、立ち止まってまず考える。そしてその思考はコーディングとは独立している。設計図——すなわち仕様——を数学で書く。なぜなら散文が曖昧なところで、数学は単純かつ厳密だからです。⁴ 「考えなければ、間違いを犯すことが確実になる」のです。²

考えているかどうかを確かめるために書け。 書くことは、ある考えが本物かどうかの試金石です。「書かずに考えているなら、考えているつもりになっているだけだ。」³ 書き留められない仕様とは、まだ実際には手にしていないアイデアなのです。

障害を正確に定義せよ。 「もしノードが嘘をついたら？」は、それをビザンチン将軍として述べ、許容限界を証明するまでは言い伝えにすぎません。厳密な定義が、不安を定理へと変えるのです。⁶

見せ方は正しさの一部である。 Paxos は、誰にも使えるようになる何年も前から正しかった。ギリシャの寓話がアイデアを埋もれさせていたからです。誰にも理解できない正しい結果は、まだエンジニアリングを終えていないのです。⁸

影響の連鎖

彼を形づくった人々

数学そのもの。 ランポートの訓練は計算機科学ではなく数学の博士号であり、彼の貢献の全体像は、直感頼みのプログラミングだった分野へ数学の基準——定義、公理、証明——を持ち込んだことに尽きます。⁶（形成的影響）

1970年代の実システムが抱えた障害耐性の問題。 航空機向けの信頼性システムに関する SRI の仕事、そしてプロトコルの途中で機械が故障するという現実的な悪夢が、彼に具体的な問題——ビザンチン障害、合意——を与えました。それらは、彼がまさに与えるべく作られていた形式的な扱いを要求したのです。⁶（直接的影響）

エドガー・ダイクストラ。 正しさはテストではなく証明によって確立される、そして並行プログラムは形式的に推論されねばならない、という信念は、ランポート以前にダイクストラのものでした。ランポートが時計の論文で受賞した賞には、ダイクストラの名が冠されています。（直接的影響）

彼が形づくった人々

あらゆる分散データベース、クラウドプラットフォーム、ブロックチェーン。 論理時計は分散ストアの競合解決を支えています。Paxos（とその子孫の Raft）は、Google の Chubby と Spanner、ZooKeeper、etcd、そして事実上あらゆるクラウドの協調レイヤーの合意の中核です。ビザンチン将軍の結果は、Bitcoin とそれ以降のあらゆる障害耐性合意プロトコルの下にある理論的な底面です。

産業界における形式手法。 Amazon Web Services は、S3、DynamoDB、その他の中核サービスを出荷する前に、TLA+ を用いて仕様化・検査することで知られています——本番ではなく設計の段階で微妙なバグを見つけるためです。ランポートの設計図論は、異端から実践へと変わりました。

この分野の語彙。 happened-before、安全性と活性、複製状態機械、逐次一貫性、ビザンチン障害——これらは分散システムの言語へのランポートの貢献というより、その言語そのものであると言ってよいほどです。

貫く筋

エドガー・ダイクストラは、プログラムを実行する前にそれが正しいと推論せよ——テストはバグの存在を示せても、その不在を示すことは決してできない——と論じました。ランポートはその直系の継承者であり、実行前の証明という考えを、逐次プログラムから、はるかに困難な並行性の世界へと運びました。そこでは、テストできないバグが例外ではなく常態なのです。バーバラ・リスコフは、データ抽象と置換可能性によって、プログラムの振る舞いに関する形式的推論を実用のプリミティブにしました。ランポートは、時間にわたるシステムの振る舞いに関する形式的推論を標準にし、オブジェクトが何を保証するかではなく、並行システム全体が常に、そしていずれ何をしなければならないかを仕様化しました。そしてドナルド・クヌースは、アルゴリズムの解析に数学的厳密さをもたらし、ほとんど余技として、仕事を厳密に書き留められるよう TeX を作りました——ランポートとほぼ完全に韻を踏んでいます。彼は同じ理由でその上に LaTeX を築き、仕様化そのものを数学的な行為にしたのです。三人の数学者は、「どうやら動くようだ」を知っていることと数えることを、いずれも拒みました。（シリーズの架け橋）

ここから私が受け取るもの

私が手放さない教訓は、思考こそが仕事であり、思考は書き留められるまで本物ではない、ということです。ランポートの設計図論が居心地悪いのは、それが正しいからです。システムが本番で壊れる理由は、コードを打ち間違えたからではほとんどありません。並行性と障害のもとでシステムが実際には何をすべきかを誰も仕様化しなかったために、コードを照らし合わせる文言が存在しなかったからなのです。規律とは、実装より前に、矛盾が目に見えるほど厳密な言語で仕様を書くことです。それは品質が唯一の変数であるというのと同じ基準です。問いは決して「ハッピーパスを通るか？」ではなく、「常に真でなければならないことを正確に述べたか——そして設計がそれを守ることを証明したか？」なのです。だからこそ私は、コードより前に PRD を書くことにこれほど重きを置きます。PRD とは、作業着をまとったランポートの仕様なのです。

私がいま身を置く世界——エージェント、ツールループ、マルチエージェントシステム——では、ランポートの教訓こそ、ほぼ誰もが省き、そして代償を払うものです。エージェントシステムはまさに分散システムです。独立したプロセス、グローバルな時計の不在、順序が入れ替わって届く、あるいはまったく届かないメッセージ、そして黙って故障する——あるいはもっと悪いことに、嘘をつく——構成要素。バグは決してプロンプトの中にはありません。順序の中にあるのです。古い状態に基づいて動く二つのエージェント、それを必要とした判断の後に結果が届くツール呼び出し、オーケストレーターが順序づけたふりをした「並行」な一対の出来事。ランポートの規律とは、壁掛け時計の直感を信じるのをやめ、因果と障害について明示的に推論し、何かを配線でつなぐ前に常に真でなければならないことを書き留めることです。作る前に仕様化する、システムをつつき回すのではなく推論する——この信念こそ、1978年の時計に関する論文から2026年のエージェントハーネスへと貫く筋であり、まさにそれゆえ私はシステムの性能と正しさを、設計で作り込む性質として扱い、後でデバッグして取り戻すことを期待する性質としては決して扱わないのです。

FAQ

レスリー・ランポートのエンジニアリング哲学とは何ですか？

ランポートの信念は、並行システムと分散システムは直感で推論するにはあまりに繊細であり、だからこそコードを書く前に、建築家がレンガを積む前に設計図を描くように、紙の上で数学を用いて考えなければならない、というものです。ソフトウェアの設計図とは仕様であり、数学は手に入る最も厳密な言語だからこそ、数学で書かれます。⁴ その根底にあるのは時間に対する立場です。分散システムには信頼できるグローバルな時計が存在しないため、計算の真の構造は因果——何が何を引き起こしたか——であって、物事がいつ起きたかではないのです。⁵ 「考えたからといって、間違いを犯さないとは限らない」と彼は言いました。「だが、考えなければ、間違いを犯すことは確実になる。」²

ランポート時計と happened-before 関係とは何ですか？

happened-before 関係は、分散システムにおける因果をランポートが形式化したものです。出来事 A が出来事 B より happened-before するのは、両者が同じプロセス上にあり A が先である場合、あるいは A がメッセージを送り B がそれを受信する場合、あるいはそれらを連鎖させた場合です。⁵ これはあくまで半順序です——異なるプロセス上にあり、それらを結ぶメッセージのない二つの出来事は真に並行であり、どちらが先だったと主張できる正しいシステムは存在しません。⁵ ランポート時計はこれを、プロセスごとのカウンターで実装します。あらゆる出来事ごとにそれを増やし、送出する各メッセージにその値を刻み、受信時には自分の値とメッセージのタイムスタンプの大きい方より1だけ大きい値へカウンターを進めます。⁷ その結果が、因果と整合した一連のタイムスタンプ——ベクトル時計と現代の分散競合解決の基礎です。

Paxos とビザンチン将軍問題とは何ですか？

Paxos は合意のためのランポートのアルゴリズムです——信頼できない、故障しうる一群の機械に、複製ログの次のコマンドのような単一の値へ合意させるもので、ほぼあらゆる現代の分散システムの協調レイヤーを支えています。よく知られているように、彼は最初それを架空のギリシャ議会についての寓話として発表しました（「The Part-Time Parliament」、ACM TOCS 1998年）。その冗談がアイデアをあまりに覆い隠したため、彼はやがて2001年に「Paxos Made Simple」として書き直しました。⁸ ビザンチン将軍問題（ランポート、ショスタク、ピース、1982年）は、最も厄介な障害モード——単にクラッシュするのではなく嘘をつき、矛盾した情報を送る構成要素——を、裏切り者が合意を妨害するなかで作戦に合意しようとする将軍たちとして定義し、システムが許容できる裏切り者の数を証明します。⁶ これがブロックチェーン合意の理論的な根です。

レスリー・ランポートはなぜチューリング賞を受賞したのですか？

ACM は2013年の A.M. チューリング賞をランポートに、「分散システムおよび並行システムの理論と実践への基礎的貢献、とりわけ因果と論理時計、安全性と活性、複製状態機械、逐次一貫性といった概念の発明に対して」授与しました。⁶ その授賞理由は彼の仕事の幅広さを捉えています。彼は分散コンピューティングを言い伝えから、厳密な定義と証明を持つ科学へと変え、この分野の語彙の多くを与え、「コードを書く前に仕様化する」を実用的な規律にするために TLA+ という仕様記述言語を生み出し——そしてクヌースの TeX を土台に、科学と数学にわたって標準となった組版システム LaTeX を書きました。⁶

出典