Image backend outage — the AI image backend (qwen/qwen-image-3) produced garbled or missing teaching text on every roll this run, so this archive card is the text-only version. The teaching content below is complete and final.
1. What a consistent cut is — causality, not agreement
You cannot stop the world to photograph it, yet you need a global state that never shows an effect before its cause. The Chandy–Lamport snapshot takes a CUT: one local state per process, plus one channel state per link.
The cut is consistent iff no recorded receive lacks its recorded send.
The forbidden shape: P2 recorded after receiving, P1 recorded before sending the same message — a state the system could never have logically occupied.
Consistency here is causal — not agreement, not locking, not a quorum vote.
Do not conflate with Lamport/vector clocks: clocks order events; this algorithm captures state. Same author, different tool.
A consistent cut = one where every receive you see also has its send.
2. The marker protocol — how the cut is actually taken
The marker is the trick. It rides the same channels as real messages and carves the instant of the cut:
The initiator records its local state, then emits a marker on every outgoing channel — before any later application message.
First marker arriving at process Pj: Pj records its state and forwards the marker on its own channels.
A later marker on a channel: stop recording that channel.
The channel's snapshot content = application messages received between the local record and the first marker — exactly the messages in flight at the instant of the cut.
Ordering rule: the marker always goes out before any later app message. That single rule is what keeps the cut consistent.
3. What it assumes — and what the slides leave out
FIFO is load-bearing. A marker that overtakes an app message loses that message from the snapshot — a silently corrupted cut.
Strong connectivity makes markers reach everyone, so the snapshot terminates. Every process takes part.
Real anchor the slides omit: Flink checkpoint barriers and Kafka Streams' consistent subsnapshot are Chandy–Lamport markers. Exactly-once = roll back to the last consistent snapshot.
The honest costs: markers can stall on busy channels, and buffered channel state costs memory and backpressure. That is precisely why Flink later invented UNALIGNED checkpoints.
4. The honest test — falsify it, don't assert it
Run the experiment and the FIFO dependency stops being a claim:
Stand up two processes with one causal edge; run the protocol repeatedly.
Enumerate all 2k interleavings of the record points. The algorithm's cut must never be one where a receive is recorded without its send.
Deliberately break FIFO (reorder one channel). A message must visibly vanish from the snapshot — the failure mode is demonstrated, not asserted.
If both invariants hold — no receive-without-send across every interleaving, and a vanished message on a reordered channel — the FIFO dependency is demonstrated. If a cut ever shows the paradox shape, the algorithm is wrong as implemented.
Practice next: pick one Flink barrier in a pipeline you know and name the Chandy–Lamport step it is doing.