A distributed snapshot is not a pause button.

That is the useful part. If the only way to inspect a distributed system were to stop every process at the same physical instant, many of the systems we care about would be uninspectable in exactly the moments we most need evidence. There is no single clock worth trusting. Messages are in flight. One machine can be between “sent” and “delivered” while another has already moved on.

The question Chandy and Lamport asked in 1985 was sharper than “can we take a picture?” It was:

can processes record local states and channel states
so the assembled picture is a possible global state?

The answer is yes, under a precise model: finite processes, directed channels that are reliable and FIFO, no shared memory, no shared clock, and arbitrary but finite message delay.1 The algorithm does not halt the underlying computation. It adds marker messages.

That sounds too small to work. It works because the snapshot is not trying to find an actual simultaneous instant. It is trying to draw a consistent cut through a partial order.

What A Cut Is

Lamport’s happened-before relation gives the evidence rule for message-passing systems: local order on a process matters, a send happens before the matching receive, and the relation is transitive.2 A global snapshot chooses a prefix of events from each process. Draw a vertical line through each process’s timeline. The union of the events to the left of those lines is a cut.

A cut is consistent when it never contains a receive without also containing the corresponding send:

\[\operatorname{recv}(m) \in C \implies \operatorname{send}(m) \in C.\]

That rule is the whole moral center. If a snapshot says process q has already received a token but process p has not yet sent it, the picture is not a possible global state. It is an artifact of observation.

The other direction is allowed. A cut may contain the send but not the receive. That means the message is in the channel state:

sent before sender's recorded state
not received before receiver's recorded state
therefore recorded as in transit

So a global state is not just the set of process-local states. It is:

local state of every process
+ contents of every channel crossing the cut

This is the part casual explanations often rush past. The channels are not implementation detail. They are where conservation laws go when processes are photographed at different logical times.

The Marker Rule

In the Chandy-Lamport algorithm, any process can start a snapshot. When it starts, it records its local state and sends a marker on each outgoing channel before sending more application messages on those channels.

Then each receiver applies two rules:

on first marker:
  record local state
  record the marker's incoming channel as empty
  send markers on all outgoing channels
  record application messages arriving on other incoming channels

on later marker for channel c:
  stop recording channel c

The phrase “marker’s incoming channel as empty” is doing real work. Because the channel is FIFO, any application message sent on that channel before the marker would have arrived before the marker. If the receiver sees the marker first, there is no older message hiding behind it on that channel.

For the other incoming channels, the receiver has recorded itself but has not yet seen the boundary marker from those senders. Any application message that arrives in that interval belongs to the channel state. It was sent before that sender’s cut and received after this receiver’s cut.

The marker is not a lock. It is a receipt that says:

everything before me on this FIFO channel belongs before the sender's cut
everything after me belongs after it

Lab: Catch The In-Transit Message

The lab below simulates three processes that transfer conserved tokens. A process that sends a token subtracts it immediately; the receiver adds it when the application message arrives. The snapshot should preserve the total number of tokens by adding recorded local balances and recorded channel messages.

Turn FIFO channels off after looking at the default run. The marker may overtake an older application message on the same channel. The audit then fails for the right reason: the original algorithm’s channel assumption has been removed.

Application message Marker message Local record Recorded channel message

Deterministic simulation. The audit checks token conservation, receive closure, and whether every sent-before/received-after message appears in channel state.

At the default setting, the snapshot starts at P0 around time 8. The lab’s processes begin with token balances [18, 14, 12], so the conserved total is 44. The recorded local balances alone usually do not add to 44. That is not a failure. The missing mass is sitting in recorded channel state.

The audit asks three questions:

1. Did the snapshot complete?
2. Does every recorded receive have its send recorded?
3. Is every sent-before / received-after application message in channel state?

With FIFO channels on, those checks pass. With FIFO channels off, the marker can arrive before an older application message on the same channel. Then the receiver closes that channel too early. The later application message was sent before the sender’s cut but is no longer recorded as channel state. The total can go missing.

You can reproduce the audit from Node:

const lab = require("./assets/js/chandy-lamport-lab.js");
const EXPECTED_CASE_SHAPE = [
  "default FIFO:expected=true:snapshot=44:channelAmount=14:channelMessages=7:appMessages=26:missing=0:overtakes=0:checks=7/7",
  "late starter FIFO:expected=true:snapshot=44:channelAmount=24:channelMessages=11:appMessages=31:missing=0:overtakes=0:checks=7/7",
  "early starter FIFO:expected=true:snapshot=44:channelAmount=9:channelMessages=5:appMessages=19:missing=0:overtakes=0:checks=7/7",
  "non-FIFO marker overtake:expected=false:snapshot=25:channelAmount=2:channelMessages=1:appMessages=26:missing=10:overtakes=10:checks=6/6"
];
const EXPECTED_CHECK_NAMES = {
  fail: [
    "snapshot completes",
    "pass state matches expectation",
    "token ledger matches pass state",
    "no receive without send",
    "marker overtake matches expectation",
    "missing channel messages expose FIFO violation"
  ],
  pass: [
    "snapshot completes",
    "pass state matches expectation",
    "token ledger matches pass state",
    "no receive without send",
    "marker overtake matches expectation",
    "no missing channel messages",
    "no extra channel messages"
  ]
};
const EXPECTED_CHECK_SHAPE = EXPECTED_CASE_SHAPE.flatMap((shape) => {
  const label = shape.split(":expected=")[0];
  const names = shape.includes(":expected=true:")
    ? EXPECTED_CHECK_NAMES.pass
    : EXPECTED_CHECK_NAMES.fail;
  return names.map((name) => `${label}:${name}:true`);
});
const EXPECTED_CASES = EXPECTED_CASE_SHAPE.length;
const EXPECTED_CHECKS = EXPECTED_CHECK_SHAPE.length;

function sameList(actual, expected) {
  return actual.length === expected.length &&
    actual.every((value, index) => value === expected[index]);
}

function caseShape(row) {
  return `${row.label}:expected=${row.expectedPass}:snapshot=${row.snapshotTotal}:` +
    `channelAmount=${row.channelAmount}:channelMessages=${row.channelMessages}:` +
    `appMessages=${row.appMessages}:missing=${row.missingChannel}:` +
    `overtakes=${row.markerOvertakes}:checks=${row.passedChecks}/${row.totalChecks}`;
}

function checkShape(row) {
  return row.checks.map((check) => `${row.label}:${check.name}:${check.passed}`);
}

const audit = lab.auditChandyLamportLab();
const shape = {
  cases: audit.cases.map(caseShape),
  checks: audit.cases.flatMap(checkShape)
};
const shapeErrors = [];
if (!sameList(shape.cases, EXPECTED_CASE_SHAPE)) {
  shapeErrors.push({ name: "cases", actual: shape.cases, expected: EXPECTED_CASE_SHAPE });
}
if (!sameList(shape.checks, EXPECTED_CHECK_SHAPE)) {
  shapeErrors.push({
    name: "checks",
    actual: shape.checks,
    expected: EXPECTED_CHECK_SHAPE
  });
}
const failedCases = audit.cases.filter(
  (row) => !row.passed || row.passedChecks !== row.totalChecks
);
if (shapeErrors.length ||
    !audit.ok ||
    audit.cases.length !== EXPECTED_CASES ||
    audit.total !== EXPECTED_CASES ||
    audit.totalChecks !== EXPECTED_CHECKS ||
    failedCases.length ||
    audit.passed !== audit.total ||
    audit.passedChecks !== audit.totalChecks) {
  throw new Error(JSON.stringify({
    shapeErrors,
    failures: audit.failures,
    failedCases,
    totals: {
      rows: audit.cases.length,
      passed: audit.passed,
      passedChecks: audit.passedChecks,
      total: audit.total,
      totalChecks: audit.totalChecks
    }
  }, null, 2));
}

console.log(`${audit.passed}/${audit.total} audit cases and ` +
  `${audit.passedChecks}/${audit.totalChecks} checks passed`);
console.table(audit.cases.map((row) => ({
  scenario: row.label,
  expected: row.expectedPass ? "pass" : "fail",
  snapshotTotal: row.snapshotTotal,
  channelAmount: row.channelAmount,
  missingChannel: row.missingChannel,
  markerOvertakes: row.markerOvertakes,
  passed: row.passed
})));

The current deterministic grid has three FIFO cases that preserve the token ledger and one non-FIFO case that is supposed to fail the protocol invariant. The audit itself passed 27/27 named checks, including the expectation that the non-FIFO run exposes missing channel messages. On that failing case, the marker overtakes ten older application messages and the snapshot total drops from 44 to 25.

The source is intentionally small: assets/js/chandy-lamport-lab.js.

The Conservation Proof Sketch

For a channel (c = p \rightarrow q), let:

n  = messages sent on c before p records
m  = messages received on c before q records

A consistent channel state should contain exactly the messages numbered (m+1, \ldots, n). If (n=m), the channel is empty at the cut. If (n>m), the difference is precisely the in-transit suffix. If (m>n), the receiver’s snapshot contains a message whose send is outside the sender’s snapshot, which is impossible for a consistent cut.

The marker makes the receiver learn where (n) is without asking the sender’s clock. Sender p records, sends the marker on c, and sends no further application messages on c before that marker. Since c is FIFO, receiver q will receive all pre-marker application messages before the marker.

There are two cases.

If q receives the marker before recording its own local state, it records itself immediately and records channel c as empty. All application messages from p that preceded the marker have already been received, so there is no sent-before/received-after suffix on c.

If q already recorded its local state, it has been logging application messages arriving on c. When the marker arrives, those logged messages are exactly the ones sent before p recorded and received after q recorded. That is the channel state.

Do that independently for every directed channel, and the assembled state obeys the receive-closure rule. Chandy and Lamport’s proof phrases the result slightly differently: even if the recorded state did not occur as a literal state in the original run, there is a permutation of independent events in which it does occur between initiation and termination.1 That is the right notion of “meaningful” in a partial order.

Stable Properties Are The Use Case

The original paper motivates snapshots with stable-property detection. A stable property is one that remains true once it becomes true: termination of a phase, deadlock under a fixed wait relation, or loss of all tokens in a token ring are examples in the paper’s model.1 If a stable property is true in the recorded global state, then it was not created by the observer’s bad timing.

This does not mean arbitrary predicates are easy. Global predicate detection is subtle because many predicates are not stable, and because different consistent cuts can disagree about transient conditions. Mattern’s later work on virtual time and global states is useful background here: distributed time is better understood as a partial order, often a lattice of possible cuts, rather than a single line that every observer can agree on.3

The snapshot algorithm gives you one well-formed point in that structure. It does not give you omniscience.

What The Algorithm Does Not Promise

It does not promise a wall-clock instant. The recorded state can be a state that is reachable by reordering concurrent events, not a frame that physically appeared on every machine at once.

It does not make non-FIFO channels FIFO. If the transport can reorder messages, the marker needs extra sequencing machinery or a different snapshot algorithm. The lab’s failing toggle is deliberately unfair to the original algorithm: it removes an assumption the proof uses.

It does not collect the snapshot for free. The marker rules tell processes what to record. A real system still needs to gather the recorded local and channel states, handle membership, bound buffers, decide how to name concurrent snapshots, and integrate the result with checkpointing or monitoring.

It also does not turn an unstable predicate into a stable one. If you ask “is queue length currently above 100?” a consistent cut avoids impossible observations, but the answer may change immediately. The stable-property framing matters because it tells you when a positive observation can safely be treated as durable.

The Debugging Shape

What I like about the algorithm is that it is honest about observation. It does not pretend that physical simultaneity is available. It does not compress a partial order into a scalar timestamp and then forget what was lost. It records the pieces that make the cut meaningful:

process prefixes
message edges crossing the boundary
FIFO markers that delimit those edges

That is a good debugging habit outside distributed-systems theory too. When a measurement spans multiple actors, ask what boundary it actually drew. Ask what state crossed that boundary. Ask which assumptions make the boundary well-defined.

The marker is tiny. The accounting it permits is not.

  1. K. Mani Chandy and Leslie Lamport, “Distributed Snapshots: Determining Global States of Distributed Systems”, ACM Transactions on Computer Systems, 3(1), February 1985. The paper states the FIFO channel model, gives the marker sending and receiving rules, and proves the recorded global state is meaningful in the computation’s partial order. ↩ ↩2 ↩3

  2. Leslie Lamport, “Time, Clocks, and the Ordering of Events in a Distributed System”, Communications of the ACM, 21(7), July 1978. ↩

  3. Friedemann Mattern, “Virtual Time and Global States of Distributed Systems”, in Proc. Workshop on Parallel and Distributed Algorithms, 1989. ↩