Safety 與 Liveness：系統正確，究竟保證了什麼？

一個系統只要永遠不產生結果，就可能避開所有錯誤結果；另一個系統也可能回覆很快，卻讓不同節點得到互相衝突的答案。因此，一份有用的規格必須同時說清楚：哪些結果絕對不能發生，以及哪些進展最終必須發生。

這就是 safety 和 liveness 各自處理的問題。它們描述執行過程的性質，不是效能指標。

1. 先把保證寫清楚

「終態結果」也要先定義：可以是成功、拒絕，還是永久失敗？如果規格要求的是成功執行，隨便回一個錯誤不能算完成承諾。

「最終」不帶固定期限。「五秒內完成」是另一個更強的規格，也需要定義時間模型。

2. 用有限前綴分辨兩者

Safety 違反會留下 finite bad prefix，有限的錯誤前綴：執行到某個有限步驟後，無論接下來怎麼做，都無法讓這段歷史重新符合規格。兩個互相衝突的 decision 一旦出現，之後重新一致也抹不掉先前的違反。

純粹的 liveness 沒有這樣的有限錯誤前綴。等待一段有限時間後，仍可能在下一步完成；違反「最終完成」的，是把完成永遠推遲的執行。Alpern 與 Schneider 在 Defining Liveness 中將這個區別形式化。

看三段執行歷史：

Safety 失敗：
接納請求 R → 提交 R → 再次提交 R
                       ↑ 有限步驟已足以證明重複

Liveness 失敗：
接納請求 R → 重試 → 重試 → 重試 → ……永遠繼續

成功完成：
接納請求 R → 重試 → 重試 → 提交 R

看到十次重試，不等於看到一個無限執行。Timeout 能指出營運異常或超過約定期限；但規格若沒有 deadline，光憑「已經等很久」，不能證明 eventual completion 已被違反。

若承諾改成「五秒內回覆」，超過期限仍未回覆就已經是有限反例。因此，在帶有時間的 execution 模型中，有界回應可以表達成 safety 條件。

3. 同一個狀態機，兩種證明責任

想像一個簡化 worker，負責處理已接納的請求。提交效果與記錄完成狀態在同一個原子轉移中發生。

flowchart LR
  A["已接納"] --> P["Pending"]
  P -->|暫時失敗| P
  P -->|帶條件的原子提交| C["完成一次"]
  C -->|重複請求回傳已存結果| C
  C -.->|禁止的第二次效果| X["Safety 違反"]

Safety 可以透過 invariant，不變條件來證明：

committedEffectCount(requestId) ≤ 1

先確認初始狀態符合它，再確認每個允許的狀態轉移都保留它。在這個模型裡，帶條件的原子提交只允許計數從 0 變成 1；重複請求直接取回已存結果。多個 worker 分別「先檢查，再執行」，並不足以建立同樣的不變條件。

Retry loop 則提出另一個問題：什麼會迫使請求離開 Pending？保持計數不超過 1，沒有回答這件事。一個永遠不提交的 worker，可以滿足這項 invariant，卻違反進度要求。

套用到真正的實作時，必須說清楚原子操作的邊界。資料庫 transaction 不會自動涵蓋外部服務的副作用；invariant 要描述程式實際能保證的範圍。

4. 有路可走，不代表一定會走到

狀態圖裡有從 Pending 到 Completed 的路，也有永遠停在 Pending 的循環。前者只能證明「完成是可能的」，不能證明系統「保證完成」。

Liveness 保證必須涵蓋模型及其假設允許的每一個執行。常見的前提包括：

• Worker 不會永久故障。
• 必要的相依服務最終恢復可用。
• 已送出的訊息最終會被交付。
• 一直具備執行條件的處理步驟，最終會被排程執行。

最後一項是一種 weak fairness，弱公平性。沒有它，scheduler 可以永遠忽略已經準備好的 worker。弱公平性適用於「持續可執行」的 action；如果 action 只間歇性具備條件，可能需要更強的公平性假設，或改變設計。

這些前提需要明寫。若模型允許相依服務永遠不可用，「一直 retry，總有一天會成功」就不構成證明。

對有限批次工作，可以用剩餘任務數做進度論證：數量不增加，而且只要還有任務，就保證最終有一個完成；反覆下降後便會到零。光是定義一個計數器還不夠，真正要證明的是「必定會下降」。

5. 非同步系統為什麼難以精準判斷故障

Detector 一直沒收到 P 的訊息，可能是 P 已故障，也可能是 P 正常、訊息只是延遲。如果規格要求最終偵測到故障，它必須在某個有限觀察之後做出懷疑；但在完全非同步模型中，正常節點也可能延遲同樣長的時間。

因此，在允許 crash 且延遲沒有上限的模型裡，完美的 strong accuracy 與 strong completeness 無法同時保證。Timeout 是操作上的決策，並沒有把沉默變成故障證明。

Consensus 也有相關界線。Paxos 在其故障假設內保護 agreement，但 termination 需要能讓進度發生的額外條件，例如穩定的 proposer 能與 quorum 通訊。它不保證每一種完全非同步 execution 都會最終做出決定。可接著看 Consensus 與 Paxos，以及 FLP 證明。

6. Stable predicate 關心的是「成立後會不會消失」

Global state 上的 predicate P 若符合以下條件，就是 stable：

P(S) 成立，則所有從 S 可到達的 S′ 都滿足 P(S′)

Stability 與 safety、liveness 是不同的分類。穩定條件可能是期待的「計算已完成」，也可能是在模型中無法自行解除的 deadlock。

flowchart LR
  A["計算仍在進行"] --> B["所有 process passive<br/>且沒有工作訊息在途中"]
  B -->|沒有新外部工作| B
  C["Process 互相等待"] --> D["封閉的循環等待"]
  D -->|沒有中止或復原動作| D

圖上的前提不能省略：

• 終止對封閉計算是穩定的：沒有新的外部工作，而且 passive process 只能被收到的工作重新啟動。
• Deadlock 只有在模型不含 timeout、取消或復原轉移時，才會持續成立。
• 判斷物件是否已不可達，也要計入訊息中攜帶的 reference，不能只查看各 process 現存的 reference。

「Deadlock freedom」這類名稱可能隱藏不同規格。「永遠不進入這個封閉死鎖狀態」是 safety；「每個等待中的請求最終都會前進」是 liveness。先寫出實際承諾，再分類。

7. Global snapshot 可以證明什麼

Chandy-Lamport snapshot 記錄包含 channel state 的 consistent cut。以 termination detection 為例：

如果 stable predicate 在 snapshot 中為真，它也會在後續可到達的狀態中維持為真。如果當下為假，之後仍可能變真，因此可能需要再拍一次。Snapshot 偵測一個條件，不會自行推動計算，也不能證明所有未來 execution 都符合某個 liveness 承諾。

自己檢查一次

1. 一直 retry 就保證 liveness 嗎？ 還需要確保重試有成功的可能，而且最終確實會獲得執行機會。
2. 重複扣款後退款，就修復 at-most-once safety 了嗎？ 退款能補償業務結果，但不能抹除歷史中已經發生的重複效果。
3. Safety 和 liveness 永遠不能兼得嗎？ 不是。不可能性定理依賴具體模型與規格；在合適假設下可以同時成立。
4. 所有節點都閒置，就代表終止嗎？ 還要沒有工作訊息在途中，並且沒有新的工作能進入計算。

整理自 UIUC Cloud Computing Concepts, Part 1 的〈Safety and Liveness〉及 global snapshot 系列投影片與逐字稿。有限前綴的區別參考文中連結的 Alpern–Schneider 論文；worker 例子為說明模型。