2013 Leslie Lamport —— 時間不存在，順序才是真相#

「分佈式系統裡，兩台機器甚至無法就『現在幾點』達成一致。 Lamport 的解法震驚且優雅：那就別用時間，用因果順序。」

案件檔案#

1970s，多機器協作的系統（SRI、PARC、Sutherland 的實驗室網路）出現怪現象：同一事件在 A 機器與 B 機器的日誌裡 先後不同。物理時鐘不可信（漂移、延遲），謎題： 沒有全局時鐘，系統還能講道理嗎？

happens-before：a → b 若 (a,b 同機且 a 先) 或 (b 收到 a 的訊息)
Lamport 時鐘：C(a) < C(b) 保證 a → b
  本地：C ← C+1；送訊息帶時間戳；收訊息：C ← max(C, ts)+1

系統的正確性只需因果序，不需牆上時鐘——分佈式系統理論的第一原理。向量時鐘（1988）隨後補全：反方向也成立（當且僅當）。

叛徒將軍會送出矛盾命令。定理：

n 台機器容忍 f 台任意故障（拜占庭），需 n ≥ 3f + 1
（口頭訊息協定需 f+1 輪；簽名訊息可放寬）

航太（飛控電腦）率先採用；三十年後成為區塊鏈共識的理論原型。Liskov（2008 案）同年做出工程化複製方案。

多數決共識協定。故事化論文（一群希臘議員）最初被編輯退稿三次、拖了九年才發表。核心：

兩階段：Prepare(n) → Promise(n, 之前見過的最大提案)
        Accept(n, v) → Accepted（n 為最大編號即接受）
安全不變式：被選中的值 = 某個被多數承諾的值
  （編號單調 + 多數派相交 → 不得改寫已決議值）

今日的 ZooKeeper、etcd、Chubby、Spanner——雲端一致性世界的地基。

因厭倦排版手稿，寫了 LaTeX 巨集包——全球學術界意外繼承的遺產（Knuth 1974 案 TeX 的最成功介面）。
TLA+：把時態邏輯（Pnueli 1996 案）與集合論合體成規格語言，Amazon、Microsoft 用其找分佈式協定 bug ——「規格先行」的工業化。

Lamport 的方法論：把系統問題化為數學題。

並發正確性 = 線性一致性（linearizability）
  所有操作看似發生在 [invoke, response] 區間的某一瞬間
  且全序一致於實際因果 → 可判定、可測試（Jepsen 譜系）

「時間不存在，因果即序」不是怪話，而是把物理假設最小化的設計哲學：不依賴的假設，就不會背叛你。