レスリー・ランポートは、分散システムの理論と実践への基礎的な貢献で知られるアメリカのコンピューター科学者である。彼は、LaTeX文書処理システムの発明や、アクションの時相論理（TLA）の定式化を含む業績により、2013年にA.M.チューリング賞を受賞した。彼のアイデアは、現代のクラウドコンピューティング、並行プログラミング、形式検証の基盤となっている。
ニューヨークのブルックリンで生まれたランポートは、マサチューセッツ工科大学で数学を学び、1960年に学士号を取得した。その後、ブランダイス大学で1963年に修士号、1972年に数学の博士号を取得した。彼の初期の研究は、1970年代にマサチューセッツ・コンピューター・アソシエイツで働きながらコンピューター科学へと移行し、共有メッセージパッシングのみで通信するプロセスの調整について研究し始めた。
分散システムとパン屋アルゴリズム
ランポートの最初の主要な貢献は、1974年に発表されたパン屋アルゴリズムであり、複数プロセスのための相互排他プロトコルである。これは各プロセスにチケット番号を割り当て、プロセスがチケット順にクリティカルセクションに入ることを保証し、アトミックな読み取り・変更・書き込み操作がなくても相互排他を達成する。この研究は、競合状態やデータ破損が蔓延していた並行プログラミングにおける根本的な課題に対処した。このアルゴリズムは、オペレーティングシステムのコースで今も教育の定番となっている。
彼は後に、1978年の論文「分散システムにおける時間、クロック、およびイベントの順序付け」で論理クロックの概念を形式化し、因果関係（先行発生）に基づくイベントの部分順序を導入した。これにより、分散システムは物理クロックに依存せずに同期でき、一貫した状態レプリケーションが可能になった。この論文はコンピューター科学で最も引用されるものの一つとなり、データベース、ファイルシステム、クラウドインフラストラクチャの設計に影響を与えた。
Paxosと合意プロトコル
1982年にランポート、ロバート・ショスタク、マーシャル・ピースによって導入されたビザンチン将軍問題は、一部のノードが故障したり、矛盾した情報を送信したりしても、システムのコンポーネントがどのように合意に達する必要があるかを定義した。ランポートの解決策であるビザンチン故障耐性アルゴリズムは、信頼性の基準を設定した。彼はその後、1989年にPaxos合意プロトコルを開発し、障害が発生しても分散ネットワークが単一の値に合意できるようにした。これはレプリケート状態機械の基礎となっている。
Paxosは、Google CloudやMicrosoft Azureからのものを含む、多くの現代の分散データベースとサービスの基盤となっている。ランポートは、架空のギリシャの島の立法府の寓話を用いてPaxosを提示したことで知られており、この教育的スタイルは後にその採用を複雑にしたと彼自身が認めている。このプロトコルの実用的な実装は進化してきたが、その理論的枠組みは依然として標準である。
LaTeX文書システム
1970年代後半、SRIインターナショナルで働いていたランポートは、ドナルド・クヌースのTeX組版エンジンの上にマクロのセットとしてLaTeXを作成した。彼は、コンテンツとプレゼンテーションを分離し、著者が構造に集中できるようにしながら、システムがフォーマットを処理するようにLaTeXを設計した。最初のメジャーリリースは1985年に登場し、数学、物理学、工学における学術出版の事実上の標準となった。
LaTeXは、自動番号付け、相互参照、参考文献管理をサポートし、多数の専門タスク用のパッケージを備えている。1986年以来開発チームによって維持されており、プレプリントリポジトリやジャーナルでの広範な使用により、学術コミュニケーションの定番として確立された。ランポート自身が最初のユーザーガイドを執筆し、これは今も参照資料となっている。
アクションの時相論理（TLA+）
1990年代以降、ランポートは形式検証に焦点を当てた。彼は、並行システムとリアクティブシステムを記述し推論するための仕様言語であるTLA+（1999年）を開発した。TLA+は数学的論理を使用してシステム状態とそれらの間を遷移するアクションをモデル化し、エンジニアが実装前に不変条件と安全性プロパティを証明できるようにする。
TLA+は、Xerox PARCやNECでのものを含む実世界の分散プロトコルに適用され、Amazonの内部分散システムの設計に影響を与えた。ランポートはまた、TLA+にコンパイルされるアルゴリズム言語PlusCalを作成し、形式手法を実務者にとってよりアクセスしやすくした。彼の2013年のチューリング賞の受賞理由は、彼の実践的および理論的貢献の両方を称賛した。
受賞と遺産
チューリング賞に加えて、ランポートは2004年にIEEEエマニュエル・R・ピオーレ賞、2005年にダイクストラ賞（Paxosプロトコルで共同受賞）、2014年にACM SIGOPSマーク・ワイザー賞を受賞した。彼は1991年に全米工学アカデミーに選出され、1992年にコンピュータ協会のフェローとなった。彼の並行性と分散システムに関する論文は、カリキュラムと産業実践を形成してきた。
ランポートは、マサチューセッツ・コンピューター・アソシエイツ、SRIインターナショナル、デジタル・イクイップメント・コーポレーション、コンパックで働いた後、2001年にマイクロソフトリサーチに加わり、現在も主任研究員として在籍している。彼は厳密なソフトウェア仕様を提唱し続けており、その影響はオペレーティングシステム、データベース理論、プログラミング言語に及んでいる。
私生活と影響
ランポートは1941年に生まれ、ブルックリンで育った。彼は数学者で論理学者のアラン・チューリングを知的インスピレーションとして挙げている。鋭い機知で知られ、数学とコンピューター科学に関するユーモラスなエッセイを発表しており、「並行性のコンピューター科学：初期の時代」や、「分散システム」という用語の誤用に対する有名な痛烈な批判を含む。彼の格言「分散システムとは、存在すら知らなかったコンピューターの故障が、自分のコンピューターを使えなくするシステムである」は広く引用されている。
ランポートは国際的に講演を続け、検証ツールの設計に貢献している。彼の研究は理論的抽象化と工学的実践を橋渡ししており、形式手法コミュニティとより広いソフトウェア産業の両方が彼を基礎的な人物と見なしている。
category:computer-science category:distributed-systems category:formal-methods category:typesetting