FLP 不可能性：為什麼系統沒有做錯，卻可能永遠無法決定？

一台伺服器一直沒有回覆。它可能已經故障，也可能會在下一次 timeout 後立刻回應。在完全非同步模型裡，沒有一個已知的延遲上限，能幫我們把這兩種情況分開。

這是理解 FLP 的直覺起點。證明要說的是更精確的結論：只要允許一個 process crash，就沒有確定性的共識協定，能在每一種合法的非同步執行中，同時保證 agreement、非平凡的決策與 termination。

這不代表共識永遠無法達成，而是任何聲稱滿足上述條件的協定，都存在一種合法執行，會一直無法做出決策。若想先對照同步模型下能做到什麼，可以從 Consensus 與 Paxos開始。

1. 先把模型假設放在眼前

協定必須容忍「可能有人 crash」。證明建構出的問題執行，不一定真的需要有人故障，也不需要網路永久分割、封包損壞或惡意副本。

Timeout 為什麼無法解決模型上的問題？

對任何有限的 T，三種情況都可能成立。Timeout 可以觸發新的嘗試，卻不能把不確定性變成「B 已死亡」的證明。這個觀察只是直覺，不是完整證明：聰明的演算法可能根本不等 B。FLP 必須連這類確定性演算法也一起涵蓋。

2. 證明研究的是 configuration，不是票數

Configuration 包含所有 process 的本地狀態，加上所有尚未送達的訊息。一次 event e = (p, m)，代表把 m 交給 p、執行確定性的本地計算，再把產生的訊息放進網路。Process 也可以執行沒有收到訊息的一步。Schedule 則是一連串 event。

對某個 configuration C，考慮從它出發，所有合法後續執行能到達的決策：

• **0-valent：**後續只可能決定 0。
• **1-valent：**後續只可能決定 1。
• **Bivalent：**存在能決定 0 的後續，也存在能決定 1 的後續。

flowchart TD
    C["Bivalent C：結果尚未固定"] -->|"排程 S0"| Z["0-valent：只剩 0 可達"]
    C -->|"排程 S1"| O["1-valent：只剩 1 可達"]
    Z --> D0["決定 0"]
    O --> D1["決定 1"]

圖中是不同的可能執行，不是同一次執行產生兩個結果。Bivalent 也不代表一半的人投 0、一半投 1；它描述整個全域狀態還能通往哪些決策。

在 univalent configuration 中，某個 process 仍可能尚未知道結果。反過來說，一旦有不可撤回的決策發生，agreement 就要求此後只能通往相同結果，所以 configuration 必須是 univalent。

3. 一開始一定存在 bivalent configuration

用反證法，先假設每個初始 configuration 都是 univalent。以三個輸入 bit 為例，每次只改一個 process 的輸入，可以把全 0 連到全 1：

000  -- 改 A -->  100  -- 改 B -->  110  -- 改 C -->  111

這些箭頭是在比較不同的初始輸入，不是程式執行的步驟。依一般 validity 條件，000 必須走向 0，111 必須走向 1。因此這條鏈上，一定存在相鄰的 0-valent 與 1-valent configuration。更一般的證明只需要非平凡性，以及初始輸入 configuration 之間的連通性。

這一對狀態只在某個 process p 的輸入不同。現在讓 p 在執行任何一步之前就 crash。其餘 process 的狀態相同，在同一個排程下也會收到相同訊息。協定既然保證能容忍一次 crash，就必須讓其他人最終決定；又因為協定是確定性的，兩邊必須做出同樣的決策。

但我們剛剛假設，一邊只可能決定 0，另一邊只可能決定 1，矛盾。因此，至少有一個初始 configuration 是 bivalent。這裡不是說兩個全域狀態真的相同：p 的狀態仍不同，只是其他正在執行的人無從觀察這個差異。

4. 可以交付某個待處理事件，同時保留 bivalence

下一個 lemma 比「把關鍵訊息一直拖著不送」更強：從 bivalent C 出發，對任意一個可執行的 event e，都能先執行有限個其他 event，再執行 e，最後仍停在 bivalent configuration。

先暫緩 e。用 S 表示不執行 e 所能到達的狀態集合，再對這些狀態分別執行 e，得到集合 D。反設 D 全部都是 univalent。因為起點 C 是 bivalent，D 中會同時有 0-valent 和 1-valent 的結果。沿著 S 裡的路徑，可以找到只差一個 event e′ 的鄰居 C0、C1，使它們執行 e 之後的結果，分別有不同 valence。

接著分成兩種情況。

情況 A：e 與 e′ 發生在不同 process

若兩個 event 本來都可執行，接收訊息的 process 又不同，就可以交換順序：先 e 再 e′，和先 e′ 再 e，會抵達同一個 configuration。這裡兩個 event 都不依賴對方才剛產生的訊息。

flowchart TD
    C0["C0"] -->|"在 p 執行 e"| D0["D0：假設是 0-valent"]
    C0 -->|"在 q 執行 e-prime"| C1["C1"]
    D0 -->|"在 q 執行 e-prime"| D1["D1：假設是 1-valent"]
    C1 -->|"在 p 執行 e"| D1

左邊的路徑讓 D0 可以到達 D1。但 0-valent 狀態不可能有 1-valent 的後代，矛盾。

情況 B：兩個 event 都發生在 p

同一個 process 上的兩個動作不能直接交換。改成考慮一段有限排程 s：讓 p 完全不執行，其他人仍能做出決策。假設中的協定既然容忍一次 crash，就必須存在這樣的決策路徑。

因為 s 不執行 p，可以把 s 移到 e 前後，也可以移到「e′ 接著 e」這一組動作的前後。把兩條分支交換順序後，會得到：已做出決策的狀態 s(C0)，竟然還能通往 0-valent 與 1-valent 兩種結果。這等於已決定的狀態仍是 bivalent，與不可撤回的 agreement 矛盾。

兩種情況都無法成立，因此 D 一定包含 bivalent configuration。我們確實可以先繞有限幾步，再交付指定的 pending event，仍保留兩種結果的可能性。這是整份證明的核心：借用假設中的 termination 保證，推出矛盾。

5. 無限執行也必須遵守公平性

如果只是永遠不把某一則訊息交給正常 process，就已經違反可靠傳遞，不足以證明 FLP。

建構方式是輪流選 process。輪到某人時，選它最早尚未收到的訊息；若沒有待收訊息，就選一個無訊息步驟。利用剛才的 lemma，先執行有限的繞路，再交付這個 event，並保留 bivalence。反覆執行，所有 process 都持續取得執行機會，每則訊息最終也會送達，但每個階段結束時仍未做出決策。FLP 原始論文第 2–3 節明確要求這些公平性條件。

flowchart LR
    B0["Bivalent C0"] -->|"有限繞路；交付 e1"| B1["Bivalent C1"]
    B1 -->|"有限繞路；交付 e2"| B2["Bivalent C2"]
    B2 -->|"持續公平排程"| More["始終沒有決策"]

不需要讓某一則訊息延遲到永遠。排程只要反覆安排有限的延遲，使下一階段完成後仍保留兩種結果即可。每則訊息最終送達，並不等於整個協定最終完成。

矛盾於是成立：原本假設每個 admissible execution 都會決定，卻建構出一個合法且永遠不決定的執行。

6. 這對實際系統有什麼意義？

Paxos透過 promise 與 quorum 證據保護既有決策；穩定 leader 和順利通訊則讓系統取得進展。成功跑完幾千次不會推翻定理，也不能證明所有排程都一定會完成。

因此，設計時值得問的是：這個系統依靠哪些假設才能前進？假設不成立時，它會做什麼？ 重試、換 leader，或暫時拒絕寫入，都可能是合理選擇，前提是沒有破壞原本要保護的 safety。

檢查理解

1. FLP 需要封包永久遺失嗎？ 不需要。不終止的執行仍可以讓每一則訊息送達。
2. Bivalent 代表還沒有人提出值嗎？ 不是。系統可能已交換很多訊息，只是兩種最終結果仍可到達。
3. 不終止的執行一定真的有人 crash 嗎？ 不一定。協定必須容忍一次可能的 crash，就足以進行證明。
4. 把 timeout 拉長能突破 FLP 嗎？ 在完全非同步模型裡，任何有限 timeout 都不能建立已知的訊息延遲上限。
5. FLP 代表 Paxos 不安全嗎？ 不是。缺少的是對所有合法執行的 termination 保證，不是決策規則的 safety。

閱讀依據

本文依據提供的 Cloud Computing Concepts, Part 1 3.4 The FLP Proof 投影片與逐字稿整理，另行繪製圖解與小範例。可靠傳遞與 admissible run 的條件，核對 Fischer、Lynch、Paterson 的 Impossibility of Distributed Consensus with One Faulty Process（JACM，1985），連結見上方。這是一份證明導讀，完整形式化細節仍以論文為準。