vault

Distributed Snapshots and the Chandy-Lamport Algorithm

17 min read

Distributed Snapshots and the Chandy-Lamport Algorithm

A distributed snapshot is a record of the global state of a distributed system — every process’s local state and every communication channel’s contents — captured without stopping the system and without a global clock. The problem is deep because, as Chandy and Lamport put it in “Distributed Snapshots: Determining Global States of Distributed Systems” (ACM TOCS, 1985), “a process can record its own state and the messages it sends and receives; it can record nothing else” (Chandy & Lamport 1985). No process can observe the whole system at one instant, and the processes cannot all record their states at the same moment because they “do not share clocks or memory.” Their algorithm solves this with marker messages: a process that initiates a snapshot records its own state and then sends a marker down each outgoing channel; each process, on seeing its first marker, records its own state and treats every channel as empty, and thereafter records on each incoming channel the messages that arrive between recording its state and receiving the marker on that channel. The astonishing result is that the assembled snapshot — process states recorded at different real-time instants, glued to channel states recorded over intervals — is nonetheless a consistent global state: a state that could have occurred, one reachable from the initial state and from which the final state is reachable, even though it may be a state that never actually occurred at any single instant of the run. This makes snapshots the foundation for detecting stable properties (deadlock, termination, token loss) and for checkpointing — and it is the direct ancestor of Apache Flink’s exactly-once checkpointing.

1. Mental Model — Photographing a Sky Full of Birds

Chandy and Lamport’s own metaphor is the clearest: the snapshot algorithm plays “the role of a group of photographers observing a panoramic, dynamic scene, such as a sky filled with migrating birds — a scene so vast that it cannot be captured by a single photograph.” The photographers each snap part of the sky at slightly different moments and paste the pieces together. Two constraints define the problem: “The snapshots cannot all be taken at precisely the same instant” (no global clock), and “the photographers should not disturb the process that is being photographed” (the snapshot must run concurrently with, but not alter, the underlying computation). “Yet, the composite picture should be meaningful.” The intellectual content of the paper is defining what “meaningful” means — a consistent global state — and showing that a purely local rule (react to markers) produces one.

sequenceDiagram
    participant p as Process p (initiator)
    participant c as Channel p→q (FIFO)
    participant q as Process q
    Note over p: record own state S_p<br/>(prerecording done)
    p->>c: send MARKER (before any further msg)
    Note over p: continue computation,<br/>may send M1, M2 after marker
    c->>q: MARKER arrives first (FIFO)
    Note over q: first marker seen →<br/>record own state S_q,<br/>record channel p→q = EMPTY
    q->>q: for OTHER incoming channels,<br/>record msgs until their marker
    Note over p,q: recorded cut = states + channel contents<br/>= a CONSISTENT global state

What it shows and the insight to take: the marker acts as a temporal divider on each FIFO channel — everything the sender put on the channel before the marker belongs to the “before” world (the pre-snapshot state); everything after belongs to the “after” world. Because the channel is FIFO, the receiver can trust that once the marker arrives, no more pre-snapshot messages can follow it. The recorded state is a clean cut between “before” and “after” on every channel simultaneously, which is exactly the definition of consistency. The receiver never needs to know when the sender recorded — the marker carries that information implicitly.

2. The System Model

A distributed system is “a finite set of processes and a finite set of channels,” modeled as a labeled directed graph with processes as vertices and channels as edges (Chandy & Lamport 1985). The channel assumptions are load-bearing:

  • Error-free and FIFO. “Channels are assumed to have infinite buffers, to be error-free, and to deliver messages in the order sent.” FIFO delivery is the crucial property the algorithm exploits — it is what lets a marker cleanly separate pre- from post-snapshot messages.
  • Arbitrary but finite delay. “The delay experienced by a message in a channel is arbitrary but finite.” There is no bound on how long a message takes — only that it eventually arrives. This is the asynchronous-network reality.
  • Channel state. “The state of a channel is the sequence of messages sent along the channel, excluding the messages received along the channel.” In other words, a channel’s state is its in-flight messages — sent but not yet delivered. This is the part that a naïve “just record every process’s state” approach misses, and getting it right is the whole trick.

A process is a set of states with an initial state and a set of events; an event is an atomic action that may change the process’s state and send or receive at most one message on one incident channel. A global state is the set of all process states plus all channel states; the initial global state has every process in its initial state and every channel empty. A sequence of events is a computation if each event can legally occur in the global state that precedes it. This machinery lets the authors define exactly what it means for a recorded state to be a legal state of some computation — the property they must prove.

Stable properties — the motivating use. A predicate y over global states is a stable property if once true it stays true: “y is said to be a stable property of D if y(S) implies y(S') for all global states S' reachable from S.” Their examples: “‘computation has terminated,’ ‘the system is deadlocked,’ and ‘all tokens in a token ring have disappeared.’” Stable properties are the natural target for snapshots because a snapshot gives you a state that lies between the moment you started recording and the moment you finished — and for a stable property, if it holds in the recorded state it necessarily holds at the end (more on this in §6).

3. Why a Naïve Cut Is Inconsistent — The n = n' Argument

Before the algorithm, the paper motivates it with the single-token conservation system: two processes p and q passing one token, so exactly one token should ever exist in the whole system. Suppose we record p’s state as “has the token,” then p sends the token to q, then we record channel c (p→q) and q’s state — but we record them after the token has been put on the channel. Now the composite shows the token in p’s recorded state and in c’s recorded state: two tokens in a single-token system — a global state “unreachable from the initial global state,” i.e. inconsistent. The inconsistency, the paper explains, “arises because the state of p is recorded before p sent a message along c and the state of c is recorded after p sent the message.”

Generalizing: let n be the number of messages p sent on c before p’s state was recorded, and n' the number sent before c’s state was recorded. If n < n', the channel captures messages whose sending was not captured — phantom messages that appear from nowhere. The dual error (recording c before p sends but p’s state after) drops messages that were sent. The requirement for consistency is therefore n = n': the channel state must be exactly the messages p sent before recording its state, minus those q received before recording its state. The marker mechanism is precisely a way to enforce n = n' without a global clock — p drops a marker right after its n-th message, and that marker tells everyone downstream where the boundary is. In the modern vocabulary of consistent cuts, a cut is inconsistent exactly when some message’s receive is on the “past” side of the cut but its send is on the “future” side — an effect recorded without its cause (Kshemkalyani & Singhal, Ch. 4). The Chandy-Lamport cut never has this property.

4. The Algorithm — Two Rules

The entire algorithm is two local rules plus an initiation. It is superimposed on the ongoing computation and must not alter it; the marker is a special control message “[that] has no effect on the underlying computation.”

Marker-Sending Rule for a process p. For each channel c incident on, and directed away from p:

“p sends one marker along c after p records its state and before p sends further messages along c.”

Marker-Receiving Rule for a process q. On receiving a marker along a channel c:

“if q has not recorded its state then begin q records its state; q records the state of c as the empty sequence end else q records the state of c as the sequence of messages received along c after q’s state was recorded and before q received the marker along c.”

Unpacking the two branches, which is where all the subtlety lives:

  • First marker q ever sees (the if branch): q had not yet recorded, so q records its own state right now. The channel c on which this first marker arrived is recorded as empty — correctly, because the marker was the very next thing after the sender’s recording boundary, so nothing pre-snapshot is still in transit behind it. Then, per the Marker-Sending Rule, q immediately floods markers out all its outgoing channels (before sending any further application messages), propagating the snapshot.
  • Every later marker (the else branch): q had already recorded its state when this marker arrives on some other incoming channel c'. The messages that arrived on c' in the interval between q recording its state and this marker arriving are exactly the messages that were in flight on c' at the snapshot instant — sent before the peer recorded, received after q recorded. q records that sequence as the channel state of c'. This is how in-flight messages are captured: not by freezing the channel, but by logging what flows in during the window bracketed by “I recorded” and “the marker got here.”

Initiation. One or more processes start spontaneously: a process records its own state and executes the Marker-Sending Rule, all without having received a marker. Any subset of processes can initiate concurrently; the algorithm still produces a single consistent snapshot.

Termination. The rules guarantee that “if a marker is received along every channel, then each process will record its state and the states of all incoming channels.” For the algorithm to finish in bounded time, two conditions must hold: (L1) “no marker remains forever in an incident input channel” (guaranteed by the finite-delay assumption), and (L2) each process “records its state within finite time” of initiation. The paper proves that “if the graph is strongly connected and at least one process spontaneously records its state, then all processes will record their states in finite time” — because a marker travels every reachable path, and every process on a path records within finite time by induction. Collecting the scattered local recordings into one global object is a separate, easy step (e.g. each process forwards what it recorded along all outgoing channels).

5. Why the Recorded State Is Consistent (Even If It Never Occurred)

The most counterintuitive fact: the snapshot S* the algorithm records “is not identical to any of the global states S₀, S₁, S₂, S₃ that occurred in the computation.” The processes recorded at different real instants, so S* is a Frankenstein state stitched from different moments. “Of what use is the algorithm if the recorded global state never occurred?” The answer is Chandy and Lamport’s central theorem.

Define an event as a prerecording event if it occurs in a process p before p records its state, and a postrecording event otherwise. Let the snapshot be initiated in global state S_ι and terminate in S_φ. The proof shows you can permute the actual computation seq into an equivalent computation seq' in which all prerecording events come before all postrecording events, by repeatedly swapping any adjacent (postrecording, prerecording) pair. Such a swap is always legal: a postrecording event e_{j-1} immediately followed by a prerecording event e_j must be in different processes, and — critically using the FIFO and marker rules — there can be no message sent at e_{j-1} that is received at e_j (if there were, the marker would have forced e_j to be a postrecording event too). So the two events are independent and can be reordered without changing the outcome.

After all the swaps, seq' is a real, legal computation, and S* is exactly the global state of seq' at the boundary — after every prerecording event and before every postrecording event. This yields Theorem 1 and its two corollaries:

  1. S* is reachable from S_ι (the state when the snapshot began) — by running the prerecording events of seq'.
  2. S_φ is reachable from S* (the state when it ended) — by running the postrecording events of seq'.

So the recorded state sits “between” the start and end of the algorithm in a very precise sense: it is a genuine state on some valid execution path from S_ι to S_φ, even if the actual run took a different path through states that were never S*. In the causal-order vocabulary, S* is a consistent cut — it respects the happens-before relation, so no recorded receive lacks its recorded send. That is all a stable-property detector needs.

6. Detecting Stable Properties

The payoff application is the stability-detection algorithm: to test a stable property y, “record a global state S*; definite := y(S*).” The output is interpreted asymmetrically, and understanding the asymmetry is essential:

  • If definite = true (the property holds in S*), then because S_φ is reachable from S* and y is stable, y holds in S_φ too — “definite = true implies that the stable property holds when the algorithm terminates.”
  • If definite = false, then because S* is reachable from S_ι, the property did not hold at initiation — “definite = false implies that the stable property does not hold when the algorithm is initiated.” But it says nothing about termination; the property could have become true in between.

This asymmetry is exactly right for the use cases. To detect deadlock or termination — both stable — you snapshot and check; a true answer is trustworthy about the present-or-future, which is what you act on. Chandy and Lamport note deadlock detection and termination detection are “special cases of the stable-property detection problem,” which is why the snapshot algorithm became a workhorse for both. (Termination detection has its own dedicated lineage — Dijkstra & Scholten — but the snapshot gives a general recipe.)

7. Alternatives and Variants

  • Lai-Yang (1987) for non-FIFO channels. Chandy-Lamport requires FIFO channels; the marker’s separating power depends on it. The Lai-Yang algorithm drops that requirement: instead of a distinct control message, it piggybacks a color bit (white/red) on every application message and computes channel state from message histories. A process is white before recording and red after; the invariant is that no red message is processed by a white process — a white process receiving a red message first records its own state (turns red). Channel state is reconstructed by having each process report the white messages it sent and received. The trade-off: Lai-Yang needs no control messages and tolerates non-FIFO channels, but requires piggybacking and message-history bookkeeping (Srivatsa 2016). Mattern’s variant uses vector-clock-style counting to the same end.
  • Coordinated checkpointing vs. the snapshot. A brute-force alternative is to halt the whole computation, record everything, and resume — correct but it stalls throughput and (in the streaming setting) is exactly what asynchronous snapshots were invented to avoid. The Chandy-Lamport contribution is precisely that you do not stop the world.
  • Uncoordinated checkpointing + message logging. Each process checkpoints independently and logs messages, reconstructing a consistent cut at recovery time. This avoids coordination overhead during normal operation but risks the domino effect (cascading rollbacks) — the opposite trade-off from coordinated snapshots.

8. Production Notes — Apache Flink’s Checkpoints

The most consequential modern use of Chandy-Lamport is Apache Flink’s checkpointing, which the Flink documentation describes as “a variant of the Chandy-Lamport algorithm called asynchronous barrier snapshotting” (Flink docs; Carbone et al. 2015). The mapping is direct: Flink’s stream barriers are Chandy-Lamport markers, injected by sources into the record stream and flowing with the data through the operator DAG. When an operator receives a barrier on an input, it records (“checkpoints”) its state; barriers then flow to downstream operators. Two production-shaping differences from the textbook algorithm are worth understanding:

  1. Barrier alignment replaces channel logging. An operator with multiple inputs waits until it has received the barrier on every input channel before snapshotting — it blocks an input once that input’s barrier arrives and buffers its records until the remaining barriers catch up. Carbone et al. prove that for an acyclic (DAG) topology this alignment means “ABS does not need to checkpoint in-flight records, but solely relies on the aligning phase to apply all their effects to the operator states,” keeping the snapshot to “the theoretical minimum (i.e., only the current state of the operators).” Where Chandy-Lamport records channel state (in-flight messages), Flink’s DAG structure lets it record nothing in transit for acyclic graphs — the alignment guarantees every pre-barrier record has already been folded into some operator’s state. For cyclic dataflows Flink does log records, but only those on identified back-edges (downstream backup), because a cycle would otherwise deadlock waiting for a barrier that circulates forever.
  2. Asynchronous, copy-on-write state. Flink’s state backends “use a copy-on-write mechanism to allow stream processing to continue unimpeded while older versions of the state are being asynchronously snapshotted,” so the checkpoint does not stall the pipeline — realizing Chandy-Lamport’s “do not disturb the underlying computation” requirement at industrial throughput.

The consistency guarantee is the same one the 1985 proof provides: a Flink checkpoint is a consistent cut of the streaming computation, so on failure the job rewinds every operator and every source offset to the same logical point, giving exactly-once state semantics — “every event will affect the managed state exactly once,” even though events are physically re-processed on recovery. Beyond Flink, the algorithm underpins distributed deadlock and termination detection and checkpoint-rollback recovery in HPC and databases — anywhere you must reason about “what is the whole system doing right now” without a clock that can answer.

Uncertain

Verify: the exact default behavior of Flink’s barrier alignment vs. unaligned checkpoints in current releases. Reason: newer Flink versions (1.11+) added unaligned checkpoints that deliberately do snapshot in-flight buffers to reduce alignment-induced latency under backpressure — closer to classic Chandy-Lamport channel recording than the 2015 ABS paper describes. To resolve: check the current Flink Checkpointing docs for the default and the unaligned-checkpoint semantics before citing specifics. The 1985 algorithm and the 2015 ABS paper claims above are quoted from primary sources and are firm. #uncertain

See Also

Graph View