Global Snapshot：從 Consistent Cut 到 Chandy-Lamport 演算法

讀取一台伺服器的狀態不難，難的是把不同時間讀到的狀態拼成一個合理的整體：訊息可能在發送端拍完 snapshot 之前離開，卻在接收端拍完 snapshot 之後才抵達。這筆訊息也必須算進去。

Chandy-Lamport 演算法讓應用程式繼續傳送訊息，同時記錄符合因果關係的全域狀態。核心工具是 marker：在一條 channel 上標出 snapshot 的邊界。

1. Global state 也包含網路裡的訊息

假設 A 與 B 的餘額分別是 100、50，A 要轉 30 給 B。這個教學模型把「發送」定義為扣款，把「接收」定義為入帳；兩個事件之間，價值由訊息攜帶。

如果只記錄中間那一列的 process state，總額會變成 120。少掉的 30 沒有消失，而是在 channel state 裡。這是用來理解訊息傳遞的模型，不是銀行轉帳系統的實作建議。

flowchart LR
  A["A：記錄餘額 70"] --> M["Channel A → B<br/>轉帳 30 還在途中"]
  M --> B["B：記錄餘額 50"]
  A -.-> T["全域總額：70 + 30 + 50 = 150"]
  B -.-> T

Global state = 每個 process 的 local state + 每條 channel 裡尚未接收的訊息。 光是同步時鐘，無法補上 channel 的資訊。

2. Consistent cut 不能留下沒有原因的結果

Cut 是在每個 process 的事件歷史上各選一個邊界。各節點不必切在同一個實際時間，但都保留邊界之前的完整事件前綴。邊界以前的事件在 cut 內，之後的事件在 cut 外。

Cut C 一致的條件是：

e ∈ C 且 f → e，則 f ∈ C

f → e 表示 f 在 Lamport 的因果順序中先於 e。既然 receive 依賴 send，納入 receive 就必須納入對應的 send。每個節點已保留完整的本地前綴，因此 message edge 是檢查跨節點一致性的關鍵。

試著調整下面兩個 cut 的位置。訊息還在途中時，channel state 會補回總額；若只包含 receive、不包含 send，就會拼出不可能的組合。手機版可在圖上左右捲動，查看兩端的事件。

Consistent cut 不一定對應某個真實的時鐘瞬間。互不依賴的事件可以重新排序而不違反因果關係；snapshot 描述的是這種等價執行中可能出現的狀態，不代表所有數值曾經在現實中同時成立。

3. Marker 能成立的前提

課程的基本模型有固定數量的 process，每一對節點之間各有一條雙向中的單向 channel。在一次 snapshot 期間：

• Process 不會故障。
• 訊息不遺失、不損壞、不重複，而且最終會抵達。
• 每條 channel 都是 FIFO；應用訊息和 marker 共用同一個順序。
• Process 能相對於自己的事件，一致地記錄 local state。
• 先只考慮一次 snapshot；多次同時執行時，需要不同 ID 和各自的記錄狀態。

最重要的本地順序是：記錄 local state 後，每條 outgoing channel 都必須先送 marker，才能送 snapshot 之後的應用訊息。 Incoming channel 的記錄也必須在處理後續訊息前開始，不能留下漏記的空隙。

不需要全域暫停或同步時鐘，但一致地擷取本地狀態，仍然是實作要解決的事。「應用程式繼續執行」不代表任意並行讀取都會自動變成原子操作。

4. 每個 process 要做什麼

發起者先記錄 local state，向所有 outgoing channel 發送 marker，並記錄每條 incoming channel 收到的應用訊息，直到該 channel 的 marker 抵達。

對其他節點，第一個 marker 同時觸發本地 snapshot，並關閉它所經過的 incoming channel。

flowchart TD
  M["在 channel c 收到 marker"] --> Q{"已記錄 local state？"}
  Q -->|否| S["記錄 local state"]
  S --> E["將 c 的狀態記為空"]
  E --> O["向外送 marker，再送後續應用訊息"]
  O --> R["記錄其他 incoming channel 的應用訊息"]
  Q -->|是| C["停止記錄 channel c"]
  C --> K["保留本地 snapshot 後、marker 前收到的訊息"]

為什麼第一個 marker 所在的 channel 記為空？FIFO 保證 marker 之前發送的應用訊息都已抵達，其效果包含在剛記錄的 local state；marker 之後發送的訊息則不屬於這次 cut。

其他 incoming channel 尚未收到 marker，代表接收端已經拍照，但還不知道發送端的邊界到了哪裡。這段期間收到的訊息要列入 channel snapshot，同時仍交給應用程式正常處理。

5. 完整推演：三個節點、六條 channel

另看一個例子：A = 100、B = 50、C = 0。用 C_BA 表示 B → A。A 發起 snapshot，但 A 給 B 的 marker 延遲抵達。B 在記錄自己的狀態之前，向 A 轉帳 m = 20。

下表列的是抵達順序。每個節點記錄 local state 時，就會送出所有 outgoing marker，並不是等到表中列出的抵達步驟才發送。

結果包含三個 local state 和六個 channel state：

Local states： S_A = 100、S_B = 30、S_C = 0
Channel state：C_BA = [轉帳 20]；其餘全部為空
總額：         100 + 30 + 0 + 20 = 150

轉帳在步驟 3 就已實際抵達，為什麼還算 in transit？因為這是相對於記錄下來的 cut：send 包含在 B 的 snapshot 裡，receive 卻不包含在 A 的 snapshot 裡。Channel state 描述這個 cut，不是記錄結束當下的網路。

後來從其他 incoming channel 收到的 marker，也不是網路把同一個封包重複送來。每個 marker 要關閉不同的 channel。三個節點共有六條單向 channel，因此這次需要六個 marker。

6. 為什麼它一定產生 consistent cut

反過來假設：某個 receive 在 cut 裡，但對應的 send 不在。發送端一定是先記錄狀態，才發送這筆應用訊息，因此它在同一條 channel 上一定先發了 marker。

由於 FIFO，接收端必定先收到 marker，於是會在接收應用訊息以前記錄自己的狀態。這又表示 receive 應該在 cut 外，與原先假設矛盾。

同樣的論證可以沿因果鏈延伸：本地前綴保留 process 內的順序，marker 保證跨 process 的結果不會搶在原因前進入 cut。如果後送的應用訊息能超越先送的 marker，這個證明就不成立；這正是基本演算法需要 FIFO 的原因。

7. Snapshot 能回答哪些問題

Snapshot 可以用在 checkpoint，以及 stable predicate 的偵測：某個條件一旦成立，在模型允許的後續轉移中就會一直成立。以封閉的分散式計算為例，終止要求所有 process 都處於 passive 狀態，且沒有工作訊息還在途中。只看到每個 worker 都閒置，仍然不夠。

每個 process 都記錄 local state、每條 incoming channel 都收到 marker 後，記錄階段才算完成。之後可以由 collector 集中收集這些片段；「把資料收齊」與「讓資料彼此一致」是不同步驟。有 E 條單向 channel 時，一次 snapshot 發送 E 個 marker，不含集中收集的流量；channel log 則取決於跨越 cut 的應用訊息量。

Snapshot 本身沒有提供持久化復原、外部副作用的原子性，或記錄期間的容錯能力。這些需要額外協定。Safety 與 Liveness 會進一步說明，一張 snapshot 能支持什麼正確性結論。

自己檢查一次

1. 本地 snapshot 後收到的訊息，都要記進 channel 嗎？ 只有該 incoming channel 的 marker 還沒抵達時才要記。
2. 後來收到其他 marker，要重拍 local state 嗎？ 不用。同一輪只記錄一次 local state；後續 marker 負責關閉 channel。
3. Channel snapshot 為空，代表實際網路一直沒有訊息嗎？ 不是。它只表示沒有應用訊息跨越這次 cut 在該 channel 上的邊界。

整理自 UIUC Cloud Computing Concepts, Part 1 的〈What is Global Snapshot?〉、〈Global Snapshot Algorithm〉與〈Consistent Cuts〉投影片及逐字稿。例子與圖解為重新整理。