A distributed system has no instant at which one observer can read every process and channel. A global snapshot therefore captures a consistent cut: local states plus messages in transit that could coexist in one execution.
What makes a cut consistent
If a cut contains a receive event, it must also contain the corresponding send. Otherwise the snapshot shows an effect without its cause. A send may be inside while its receive is outside; that message belongs to channel state.
In plain terms: money may be absent from both account snapshots only if the transfer is recorded as still in transit.
Chandy-Lamport markers
Under reliable FIFO channels:
- The initiator records its local state and sends a marker on every outgoing channel.
- A process receiving its first marker records local state, treats that incoming channel as empty, then forwards markers.
- Until a marker arrives on another incoming channel, messages received there are recorded as channel state.
- The snapshot finishes after every process and incoming channel is recorded.
The marker separates messages logically before and after the snapshot without pausing normal messages.
What snapshots are for
- distributed checkpointing and recovery;
- detecting stable properties such as termination or deadlock;
- debugging and auditing;
- measuring global state such as tokens or balances.
The result is not necessarily the state at one physical-clock instant. It is a causally valid state from the execution.
Review card
- Global state contains process state and channel state.
- A consistent cut never includes an effect without its cause.
- In-transit messages explain state crossing the cut.
- Chandy-Lamport relies on FIFO channels in its basic form.
- Markers record boundaries while application traffic continues.
Distributed system 沒有一個 observer 能在同一瞬間讀完所有 process 與 channel。Global snapshot 因此要擷取 consistent cut:能在某個 execution 合理共存的 local state 與 in-transit message。
Cut 何時 consistent
如果 cut 包含 receive event,就必須包含對應 send;否則 snapshot 有 effect 卻沒有 cause。Send 可以在 cut 內、receive 在外,此時 message 應列入 channel state。
白話來說: 轉帳金額可以同時不在兩個 account snapshot 裡,但必須被記成仍在途中。
Chandy-Lamport marker
在 reliable FIFO channel 假設下:
- Initiator 記錄 local state,向所有 outgoing channel 發 marker。
- Process 第一次收到 marker 時記 local state,將該 incoming channel 記為 empty,再轉送 marker。
- 其他 incoming channel 在 marker 抵達前收到的 message,都記為 channel state。
- 所有 process/incoming channel 記完後完成。
Marker 在邏輯上分開 snapshot 前後的 message,不必暫停 normal traffic。
Snapshot 的用途
- distributed checkpoint/recovery;
- 偵測 termination、deadlock 等 stable property;
- debugging/audit;
- 計算 token、balance 等 global state。
結果不必等於某個 physical-clock instant,而是 execution 中 causally valid 的 state。
複習卡
- Global state 包含 process state 與 channel state。
- Consistent cut 不會留下無 cause 的 effect。
- In-transit message 解釋跨越 cut 的 state。
- 基本 Chandy-Lamport 假設 FIFO channel。
- Marker 在 application traffic 繼續時記錄 boundary。