Distributed Snapshots: Determining Global States of Distributed Systems

Reference: K. Mani Chandy, Leslie Lamport (1985). ACM Transactions on Computer Systems, 3(1):63-75. Source file: chandy-lamport-1985.pdf. URL

Summary

Introduces the Chandy-Lamport distributed-snapshot algorithm: a decentralised procedure by which processes in an asynchronous message-passing system can jointly record a consistent global state without halting the underlying computation and without any shared clock. The recorded state may never have existed at a single instant, but it is reachable from the initial state and can reach the final state; in particular, it correctly detects any stable property (deadlock, termination, token loss, etc.).

The algorithm works on a strongly connected graph of FIFO channels: the initiator records its local state and sends a special marker on every outgoing channel; upon first receipt of a marker on an incoming channel, a process records its own state, records the incoming channel as empty, and propagates markers on its outgoing channels; subsequent markers terminate channel recording. The paper’s “photographers of migrating birds” metaphor became canonical for the problem. The snapshot defines a consistent cut in the happens-before order and is the foundation for distributed debugging, checkpointing, and stable-property detection.

Key Ideas

Global state = set of process states plus set of channel (message-in-transit) states
Marker messages as in-band synchronization tokens on FIFO channels
A recorded snapshot is reachable from the pre-snapshot state and reaches the post-snapshot state, even though it may never have held simultaneously
Stable properties (termination, deadlock, lost tokens) can be decided on any recorded snapshot
No shared clock, no halting of the underlying computation, fully decentralised initiation
Requires FIFO channels and eventual delivery; channel state = messages sent before marker but received after

Connections

Conceptual Contribution

Claim: A consistent global state of an asynchronous distributed system can be recorded by a fully local algorithm using in-band marker messages, without stopping the computation and without shared clocks.
Mechanism: An initiator records its state and floods markers. Each process, on first marker arrival on channel c, records its own state and treats the pre-marker messages on c as empty; for subsequent incoming channels it records the messages received after its own state-recording and before the marker as the channel’s recorded state. FIFO channels guarantee consistency of the resulting cut.
Concepts introduced/used: Consistent cut, global state, stable property, marker protocol, in-band control, distributed termination detection, distributed deadlock detection, checkpointing.
Stance: formal / algorithmic.
Relates to: Builds directly on the happens-before relation and logical clocks of Time Clocks and the Ordering of Events in a Distributed System — a snapshot is a consistent antichain in that partial order. Complements CALM Theorem, which characterises computations whose results are insensitive to message ordering and therefore need no snapshot for correctness. The flooding of markers over a connected topology is a structural cousin of Gossip Protocols, though snapshot markers carry exact-once semantics rather than probabilistic diffusion.

Tags

#distributed-systems #snapshots #global-state #stable-properties #checkpointing

CALM Theorem

Consistency As Logical Monotonicity (Hellerstein 2010 conjecture; Ameloot, Neven, Van den Bussche 2013 proof). A distributed program has a consistent, coordination-free implementation if and only if it is expressible in monotonic logic.

Monotonic programs produce a set of outputs that only grows as inputs arrive (S ⊆ T ⟹ P(S) ⊆ P(T)). Such programs are safe under missing information: any conclusion reached on a subset of inputs remains valid when more arrive. Non-monotonic programs may retract earlier conclusions, so they must wait for “all the news” — which is what distributed coordination enforces.

CALM is the positive counterpart to the CAP Theorem: it names the exact class of programs that can satisfy Consistency, Availability, and Partition-tolerance simultaneously.

Why it matters

Moves consistency from a property of storage (linearizability, serializability) to a property of programs — Confluence.

Tells programmers what kinds of features are free (monotonic: set union, counting up, set-containment) and what must be paid for (non-monotonic: set difference, strict aggregation, count-exact, deletions without tombstones).

Gives a design rule for coordination-free systems: build from monotonic primitives — CRDTs, Immutable Data Structures, Tombstones, monotonic accumulators — and only add coordination at non-monotonic boundaries.

Summary

Lamport’s seminal paper reframes time in distributed systems. Rather than depending on physical clocks that cannot be perfectly synchronized, he defines a partial order on events — the “happened-before” relation (→) — using only causality derived from local process order and message exchange. Two events are concurrent iff neither happened before the other. This reorientation showed that a distributed system’s truth about “when” is inherently relational, not absolute, mirroring the space-time view of special relativity.

Lamport then introduces logical clocks — counters per process that assign numbers to events such that a → b implies C(a) < C(b). A simple algorithm (increment on local events; piggyback timestamps on messages; bump local clock on receipt) provides this. Extending the partial order to a total order via tiebreaking by process ID enables the classic distributed mutual exclusion algorithm that uses only message passing without a central coordinator.

The final portion generalises to physical clocks, deriving synchronization bounds that tolerate clock drift and message delay. The paper is foundational: it underlies vector clocks, causal broadcast, state-machine replication, Paxos, version vectors in Dynamo/Riak, CRDT causality tracking, and distributed snapshotting.

Key Ideas

Happened-before (→): irreflexive partial order capturing causal precedence.

Concurrency: a ∦ b when neither a → b nor b → a; cannot be eliminated in a distributed system.

Logical clocks: monotone counters satisfying the Clock Condition; do not measure real time but respect causality.

Total ordering: arbitrary tie-break on process IDs yields a global total order usable for coordination.

Distributed mutual exclusion: a worked example of using total ordering of timestamped requests to implement a resource without a central arbiter.

Space-time diagrams: process lines + message arrows — a durable visual vocabulary for distributed reasoning.

Physical clock synchronization: bounded drift + bounded message delay yield clock-sync with provable error.

Connections

CAP Theorem — partitions and concurrent writes are grounded in Lamport’s concurrent events.

CALM Theorem — monotonic computation avoids the coordination that Lamport’s algorithms provide.

Keeping CALM - When Distributed Consistency is Easy

Coordination Avoidance — when → does not need to be totally ordered.

Gossip Protocols — epidemic dissemination implicitly maintains a causal partial order.

Impossibility of Distributed Consensus with One Faulty Process — FLP shows limits of coordination Lamport makes feasible in fault-free settings.

Knowledge and Common Knowledge in a Distributed Environment — epistemic reading of causal pasts.

Distributed Snapshots: Determining Global States of Distributed Systems

Summary

Key Ideas

Connections

Conceptual Contribution

Tags

Backlinks