Can You Keep a Secret? A New Protocol for Sender-Side Enforcement of Causal Message Delivery

Reference

Tong, Y., Liittschwager, N. & Kuper, L. (2026). “Can you keep a secret? A new protocol for sender-side enforcement of causal message delivery.” To appear at PaPoC 2026 (11th Workshop on Principles and Practice of Consistency for Distributed Data). arXiv:2603.14690. URL

Summary

Causal delivery guarantees that if one message causally precedes another (in the happened-before sense), no recipient sees the second before the first. There are two classic enforcement strategies. Receiver-side enforcement attaches causal metadata (e.g. vector clocks) to every message and has recipients buffer messages until their dependencies arrive — correct, but it pays a per-message metadata cost that grows with the system. Sender-side enforcement instead has senders hold messages back until it is safe to release them, avoiding the metadata overhead, but the traditional sender-side approach is overly conservative: a sender delays emitting a message until it can be sure no earlier-but-undelivered message could overtake it, stalling work that could have proceeded.

This paper introduces Cykas, a sender-side protocol that “sidesteps the conservativeness of the traditional sender-side approach by allowing eager sending of messages and constraining the behavior of their recipients.” Rather than blocking the sender, Cykas lets messages go out eagerly and shifts the obligation to recipients, who are constrained so that the causal-delivery guarantee is still preserved without per-message causal metadata. The authors implement Cykas in Rust and verify its correctness with the Stateright model checker, and report that eager sending yields performance benefits for long-running jobs — letting downstream jobs start earlier and reducing overall execution time relative to the conservative sender-side baseline.

Key Ideas

Sender-side vs receiver-side causal delivery: receiver-side buffers on causal metadata; sender-side withholds messages to avoid metadata but is traditionally conservative. Cykas keeps the sender-side metadata savings while removing the conservatism.
Eager sending + constrained recipients: the core move is to send eagerly and place the safety constraints on recipient behaviour, rather than stalling the sender until release is provably safe.
No per-message causal metadata: preserves the central advantage of the sender-side family — avoiding vector-clock-style overhead that scales poorly.
Formally model-checked: the protocol is implemented in Rust and its causal-delivery guarantee verified using the Stateright model checker.
Performance for long-running jobs: eager emission lets dependent work begin sooner, lowering end-to-end execution time compared to the conservative sender-side approach.

Connections

Time Clocks and the Ordering of Events in a Distributed System — the happened-before relation that causal delivery is defined against.
Causal Message Delivery — the property this protocol enforces.
Vector Clock — the receiver-side metadata Cykas avoids carrying per message.
Distributed Snapshots Determining Global States of Distributed Systems — companion notion of causally-consistent global state.
Gossip Protocols — epidemic dissemination that implicitly maintains a causal partial order.
Keeping CALM - When Distributed Consistency is Easy — monotonicity as the other lever for cheap consistency.
A Comprehensive Study of Convergent and Commutative Replicated Data Types — CRDT causality tracking is the receiver-side cost this work routes around.
Stateright — the Rust model checker used to verify the protocol.
ChoRus - Library-Level Choreographic Programming in Rust — same research lineage (Kuper group); Rust-based, verification-minded distributed protocols.

Conceptual Contribution

Claim: Sender-side enforcement of causal message delivery need not be conservative. By allowing senders to emit eagerly and instead constraining recipient behaviour, a protocol can keep the metadata-free advantage of the sender-side family while removing the delays that previously made it slower than necessary.
Mechanism: Cykas — eager sending paired with recipient-side constraints sufficient to preserve causal delivery without per-message causal metadata; implemented in Rust and verified with the Stateright model checker; evaluated against the conservative sender-side baseline.
Concepts introduced/used: Cykas, Causal Message Delivery, Sender-Side Enforcement, Vector Clock, Model Checking, Happened-Before.
Stance: systems / protocol design with formal verification.
Relates to: sits in the causal-delivery lineage rooted in Lamport’s happened-before and the receiver-side metadata tradition of vector clocks; shares the Rust-and-verification methodology of the Kuper group’s choreographic work (ChoRus - Library-Level Choreographic Programming in Rust, HasChor - Functional Choreographic Programming).

Tags

#distributed-systems #causality #causal-delivery #consistency #model-checking #rust #papoc

Backlinks

index

Linked Pages

HasChor - Functional Choreographic Programming

HasChor: Functional Choreographic Programming for All

Reference: Shen, G., Kashiwa, S. & Kuper, L. (2023). HasChor: Functional Choreographic Programming for All (Functional Pearl). Proceedings of the ACM on Programming Languages (PACMPL) 7(ICFP), Article 207, ICFP 2023. ACM. DOI: 10.1145/3607849. Preprint: arXiv:2303.00924 [cs.PL], DOI: 10.48550/arXiv.2303.00924. URL. Software: https://github.com/gshen42/HasChor.

Summary

HasChor is a Haskell library that brings Choreographic Programming into a mainstream functional language without a bespoke compiler. A choreography is written as a single global program — an ordinary Haskell computation in a Choreo monad — that describes the behaviour of every participant in a distributed system at once, and the library performs Endpoint Projection at runtime to derive the local program each node actually executes. The library’s central insight, given as a functional pearl, is that endpoint projection has a short and simple essence once it is expressed monadically: the same Choreo value, interpreted with respect to a particular location, naturally specialises to that location’s behaviour, with communications becoming sends on the projecting node and receives on the others.

The interface is built from a small set of choreographic operators — most importantly locally (a local computation at one node) and comm/~> (a directed communication that moves a value from one node to another, returning a located value visible only at the recipient). Located values, indexed by their owning location at the type level, statically prevent a node from using data it does not hold. Because the host language is Haskell, choreographies are first-class and higher-order: they can be passed as arguments, returned, and abstracted over their participating locations (location polymorphism), so reusable distributed protocols compose like ordinary functions. HasChor thus delivers deadlock-free-by-construction distributed code — bank services, key-value stores, and similar examples — entirely as a library, demonstrating that choreographic programming need not be confined to dedicated languages such as Choral.

Key Ideas

Choreographies as a monad: a global program is a value in a Choreo monad; ordinary do-notation expresses the joint behaviour of all participants.
Endpoint projection as interpretation: projection is performed at runtime by interpreting the one Choreo value with respect to a target location — no separate compiler — reducing EPP “to its short and simple essence”.
Located values: a @ l types a value as living at location l; the type system stops a node from accessing data it does not own, enforcing communication safety.
Core operators: locally for node-local computation and comm (~>) for directed communication, which is the only construct that moves data between locations.
Higher-order & location-polymorphic choreographies: choreographies are first-class Haskell values that can be passed, returned, and abstracted over their participants, giving modular, reusable protocols.
Library, not language: the whole approach is a Haskell library, so choreographies interoperate with the existing ecosystem and toolchain.
Functional pearl: the contribution is as much pedagogical as practical — a clean, minimal account of how projection falls out of a monadic embedding.

Connections

Conceptual Contribution

Claim: Choreographic programming can be delivered as an ordinary library in a functional host language rather than a dedicated compiler: once choreographies are embedded as values in a monad, endpoint projection becomes a short runtime interpretation, and choreographies inherit first-class, higher-order, and location-polymorphic composition for free.
Mechanism: Embed global programs in a Choreo monad; type communicated data as located values (a @ l) so the type checker enforces that nodes only touch data they own; provide locally and comm as the core operators; implement endpoint projection by interpreting the single Choreo value against a chosen location, so sends/receives specialise per node; leverage Haskell’s higher-order functions for location-polymorphic, composable choreographies.
Concepts introduced/used: Choreographic Programming, Endpoint Projection, located values, location polymorphism, higher-order choreographies, monadic embedding, Session Types
Stance: language/library design (functional pearl)
Relates to: The library-level counterpart to Choral - Object-Oriented Choreographic Programming (Giallorenzo, Montesi & Peressotti TOPLAS 2024), where Choral makes roles a type parameter and compiles to per-role Java, HasChor keeps endpoint projection inside the host language as a monadic interpretation. It is the direct precursor to ChoRus - Library-Level Choreographic Programming in Rust (Kashiwa et al.), which ports the EPP-as-interpretation idea to Rust as dependency injection. Both are named in Introduction to Choreographies (Montesi 2023) as part of the modern choreographic-programming implementation landscape, and both rest on the choreography/session-type lineage of Structured Communication-Centred Programming for Web Services and Multiparty Asynchronous Session Types.

Tags

ChoRus - Library-Level Choreographic Programming in Rust

ChoRus: Library-Level Choreographic Programming in Rust

Reference: Kashiwa, S., Shen, G., Zare, S. & Kuper, L. (2023). Portable, Efficient, and Practical Library-Level Choreographic Programming. arXiv:2311.11472 [cs.PL]. DOI: 10.48550/arXiv.2311.11472. URL. A short version, ChoRus: Library-Level Choreographic Programming in Rust (Kashiwa & Kuper), was presented at CP 2024 (Choreographic Programming workshop, co-located with PLDI 2024). Software: https://github.com/lsd-ucsc/ChoRus.

Summary

ChoRus is the first Choreographic Programming library for Rust. It carries the library-level approach pioneered by HasChor into a language without higher-kinded monadic machinery, and in doing so distils the underlying technique into a language-agnostic recipe. The paper’s first contribution is endpoint projection as dependency injection (EPP-as-DI): rather than compiling a choreography to per-node programs ahead of time, the library bundles the choreographic operators (local computation, communication, etc.) into an interface and injects a node-specific implementation at run time. Projecting the choreography onto a given participant just means running the single global program with that participant’s operator implementations supplied — communications become sends on the projecting node and receives elsewhere. The only host-language feature required is higher-order functions, so the same design transfers to many languages; in Rust the operators are bundled into a trait passed to a run method for an ergonomic API.

The second contribution is choreographic enclaves: a language construct that lets a programmer carve out a sub-choreography among a subset of participants, so that Knowledge of Choice — the obligation to inform every participant affected by a branch — is propagated only within the enclave rather than broadcast to all nodes. This makes branching choreographies more efficient by avoiding unnecessary notifications to participants that are not involved in a local decision. The authors implement both techniques in ChoRus and evaluate it on case studies and benchmarks, finding usability and performance comparable to writing the same distributed systems with conventional Rust libraries — evidence that choreographic programming can be both portable and practical at the library level.

Key Ideas

First CP library for Rust: brings choreographic programming to a systems language, as a library rather than a dedicated compiler.
Endpoint projection as dependency injection (EPP-as-DI): project by injecting node-specific implementations of the choreographic operators into one global program; needs only higher-order functions, hence language-agnostic.
Operators bundled in a trait: Rust realises EPP-as-DI by packaging the choreographic operators into a trait passed to run, giving an idiomatic, ergonomic API.
Choreographic enclaves: sub-choreographies over a subset of participants within which knowledge of choice is propagated only among enclave members, cutting unnecessary selection messages.
Efficiency of branching: enclaves localise the cost of informing participants about choices, improving performance on protocols with local decisions.
Portable & practical: case studies and benchmarks show usability and performance on par with conventional distributed Rust code.
Located values & operator interface: as in HasChor, data is tied to the node that owns it, and communication is the sole operator that moves a value between participants.

Connections

Conceptual Contribution

Claim: Library-level choreographic programming is portable and practical: endpoint projection can be implemented in essentially any language with higher-order functions by treating it as dependency injection of node-specific operator implementations, and branching can be made efficient by scoping knowledge of choice to enclaves of the participants that actually need it.
Mechanism: Express a choreography as one global program parameterised over an interface (a Rust trait) of choreographic operators; project onto a node by injecting that node’s operator implementation and running the program, so communications resolve to sends/receives per participant (EPP-as-DI); introduce choreographic enclaves that delimit a sub-choreography over a participant subset and confine selection/knowledge-of-choice propagation to it; implement and benchmark the design as the ChoRus Rust library.
Concepts introduced/used: Choreographic Programming, Endpoint Projection, endpoint-projection-as-dependency-injection, choreographic enclaves, Knowledge of Choice, located values, Session Types
Stance: language/library design with empirical evaluation
Relates to: The Rust successor to HasChor - Functional Choreographic Programming (Shen, Kashiwa & Kuper ICFP 2023): where HasChor realises endpoint projection as a monadic interpretation in Haskell, ChoRus reframes the same idea as dependency injection so it no longer depends on monads and ports to Rust, adding enclaves for efficient branching. It is a library-level sibling of the compiler-based Choral - Object-Oriented Choreographic Programming (Giallorenzo, Montesi & Peressotti TOPLAS 2024), and both are listed in Introduction to Choreographies (Montesi 2023) as part of the modern implementation landscape building on Structured Communication-Centred Programming for Web Services and Multiparty Asynchronous Session Types. Its enclave mechanism operationalises the realisability condition studied in Knowledge of Choice.

Tags

Vector Clock

(page does not exist)

Time Clocks and the Ordering of Events in a Distributed System

Time, Clocks, and the Ordering of Events in a Distributed System

Reference

Lamport, L. (1978). “Time, Clocks, and the Ordering of Events in a Distributed System.” Communications of the ACM, 21(7), 558-565. URL

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.

Conceptual Contribution

Stateright

(page does not exist)

Causal Message Delivery

(page does not exist)

Cykas

(page does not exist)

A Comprehensive Study of Convergent and Commutative Replicated Data Types

Reference: Shapiro, M., Preguiça, N., Baquero, C. & Zawirski, M. (2011). INRIA Research Report RR-7506, January 2011. (Subsequently SSS 2011 — Stabilization, Safety, and Security of Distributed Systems, LNCS 6976: 386–400.) Source file: shapiro-crdts-rr7506.pdf. URL

Summary

Shapiro, Preguiça, Baquero and Zawirski give the canonical formal account of Conflict-free Replicated Data Types (CRDTs) — replicated objects whose replicas can be updated concurrently without coordination, and which converge to a deterministic value once all updates have propagated. The paper distinguishes two equivalent specification styles: state-based / Convergent Replicated Data Types (CvRDTs), where each replica’s state forms a join-semilattice and replicas merge by joining states; and operation-based / Commutative Replicated Data Types (CmRDTs), where operations are designed to commute pairwise so that any delivery order yields the same final state under causal broadcast. They prove the two styles equivalent in expressive power and characterise Strong Eventual Consistency (SEC): the stronger sibling of eventual consistency in which all replicas that have received the same set of updates are immediately identical, with no need to wait for the system to “calm down.”

The paper catalogues a library of CRDTs spanning counters (G-Counter, PN-Counter), registers (LWW-Register, MV-Register), sets (G-Set, 2P-Set, OR-Set, LWW-element-Set), maps, sequences, and graphs, together with the design patterns (tombstones, version vectors, causal histories) that make them work. A separate axis treats delta-CRDTs and bandwidth-efficient propagation. The result is the foundational reference for coordination-free replicated state — adopted across Riak, Redis, Soundcloud’s Roshi, Akka, Automerge, and Yjs, and one of the two pillars (alongside the CALM Theorem) of the contemporary “consistency without coordination” programme.

Key Ideas

State-based (CvRDT): replica state is a join-semilattice; updates are monotone state transitions; merge is lattice join. SEC follows automatically from associativity, commutativity, idempotence of join and monotonicity of updates.
Operation-based (CmRDT): replicas exchange operations rather than states; operations must commute pairwise; causal broadcast plus commutativity yields SEC.
Equivalence theorem: every state-based CRDT can be expressed op-based, and vice versa, under appropriate delivery assumptions.
Strong Eventual Consistency (SEC): all replicas that have observed the same updates are byte-identical, regardless of order — strictly stronger than classical eventual consistency.
CRDT zoo: G-Counter, PN-Counter (counters); LWW-Register, MV-Register (registers); G-Set, 2P-Set, OR-Set, Add-Wins/Remove-Wins Sets (sets); OR-Map, RGA, LSEQ (maps and sequences); Add-only Graph (graphs). Each design choice corresponds to a different conflict-resolution policy made explicit.
Tombstones: a standard pattern for monotonising removal — instead of forgetting a removed element, mark it removed (a monotone state change).
Causal-broadcast assumption: op-based CRDTs require the network layer to deliver operations in causal order; state-based CRDTs make weaker assumptions.

Connections

Conceptual Contribution

Claim: Replicated objects can converge deterministically without coordination iff their state forms a join-semilattice with monotone updates (state-based) or their operations pairwise commute under causal delivery (op-based); the two styles are equivalent in expressive power and together yield Strong Eventual Consistency, a precise formal target for replicated data structures that is strictly stronger than classical eventual consistency.
Mechanism: Formalise replica state as a join-semilattice; prove SEC follows from join-associativity / -commutativity / -idempotence plus monotone updates; characterise op-based CRDTs via pairwise operation commutativity under causal broadcast; prove state-based and op-based formulations equivalent. Catalogue counters, registers, sets, maps, and sequences as instances; document tombstones, version vectors, and causal histories as recurring design patterns.
Concepts introduced/used: CRDTs, Strong Eventual Consistency, join-semilattice, Tombstones, Version Vector, Causal Broadcast, Eventual Consistency, CAP Theorem
Stance: foundational / formal-systems
Relates to: Foundational reference for CRDTs across the contemporary distributed-systems stack; the lattice-theoretic substrate that Logic and Lattices for Distributed Programming (Conway et al. 2012) lifts into a programming-language type system, and that Keeping CALM - When Distributed Consistency is Easy (Hellerstein & Alvaro 2019) generalises into the CALM Theorem. Where CALM gives the theorem (monotone ⇔ coordination-free) and BloomL gives a language, this paper gives the data structures: a catalogue of CRDTs that designers can drop into a coordination-free system. The G-Set / OR-Set / version-vector vocabulary is what CBCL - Safe Self-Extending Agent Communication’s SPEC-003 message-store lattice and SPEC-002 causal-protocol layer use directly. Pairs with Time Clocks and the Ordering of Events in a Distributed System (Lamport 1978) on the causal-history side and with Brewers Conjecture and the Feasibility of Consistent Available Partition-Tolerant Web Services on the impossibility-result side: where CAP says you can’t have all three of consistency, availability, and partition-tolerance for arbitrary programs, CRDTs identify a class of programs (those whose state lives in a join-semilattice) for which all three coexist.

Tags

Keeping CALM - When Distributed Consistency is Easy

Keeping CALM: When Distributed Consistency is Easy

Reference: Joseph M. Hellerstein & Peter Alvaro (2019). arXiv:1901.01930v2. Source file: ../1901.01930v2.pdf (in parent directory). URL

Summary

An accessible, updated statement of the CALM Theorem — Consistency As Logical Monotonicity: a program has a consistent, coordination-free distributed implementation if and only if it is monotonic in a formal logical sense. Monotonic programs are “safe” under missing information and can proceed without waiting: once something has been concluded, it stays concluded. Non-monotonic programs (“change their mind” in the face of new inputs) are necessarily order-sensitive and therefore require coordination to produce a single deterministic outcome.

CALM is a positive counterpart to the negative results of the CAP Theorem and the FLP impossibility. Where CAP says “you can’t always have it all”, CALM delineates the class of programs that can in fact satisfy all of C, A, and P simultaneously: exactly the monotonic ones. The theorem shifts attention away from storage consistency (linearizability, serializability) toward program consistency — Confluence: deterministic outcomes despite non-deterministic message delivery and ordering.

The paper traces the theorem’s implications for Bloom Language, Dedalus, CRDTs, coordination-free design patterns (monotonic accumulation, tombstones, immutable data), distributed garbage collection, and Amazon’s shopping-cart example. It closes with open questions: expressiveness of monotonic languages, program synthesis targeting monotonicity, repair of non-monotonic code, and a possible Stochastic CALM for near-optimum stochastic algorithms.

Key Ideas

Monotonicity ⇔ coordination-freeness ⇔ consistency (CALM)
Program consistency = confluence: same outputs regardless of message order / batching
Non-monotonic operations retract earlier conclusions, hence must wait for “all the news” — requiring Coordination Avoidance logic to know when
Formalisation via Relational Transducer networks (Ameloot, Neven, Van den Bussche)
CAP is a special case: linearizable storage is one non-monotonic operation; CALM asks the question across all programs
Practical playbook: immutable data structures, tombstones, set-monotonic accumulation, CRDTs as object-oriented monotonic types
Bloom gives syntactic monotonicity checking — a programmer writing monotonic Bloom is guaranteed coordination-free correctness

Connections

CALM Theorem
CAP Theorem
Confluence
Monotonic Logic
Coordination Avoidance
Bloom Language
Dedalus
CRDTs
Relational Transducer
Non-monotonic Reasoning
Gossip-Based Computation of Aggregate Information
Gossip-based Aggregation in Large Dynamic Networks
Extensible Distributed Coordination
Are Multiagent Systems Resilient to Communication Failures
Foundations of Logic Programming - Lloyd
Logic and Lattices for Distributed Programming — Conway et al. 2012 (BloomL; lattice-typed lifting of CALM)
Relational Transducers for Declarative Networking — Ameloot, Neven & Van den Bussche 2011 (the formal proof of CALM)
A Comprehensive Study of Convergent and Commutative Replicated Data Types — Shapiro et al. 2011 (the CRDT canonical reference)

Conceptual Contribution

Claim: A distributed program is consistent and coordination-free iff it is expressible in monotonic logic — a tight, provable characterisation that converts “distributed consistency is hard” into a precise question about a program’s logical shape.
Mechanism: Formalise programs as networks of Relational Transducers (Ameloot et al.); define Confluence as program-level determinism under non-deterministic delivery; prove biconditional between confluence and monotonic-logic expressibility.
Concepts introduced/used: Monotonic Logic, Confluence, Coordination Avoidance, Relational Transducer, Bloom Language, Dedalus, CRDTs, CAP Theorem, Immutable Data Structures, Tombstones, Stochastic CALM
Stance: foundational / survey
Relates to: Provides the theoretical companion to the Gossip Protocols cluster (Gossip-Based Computation of Aggregate Information, Gossip-based Aggregation in Large Dynamic Networks) — gossip aggregation with mass conservation is exactly a monotonic accumulation, hence coordination-free. Frames why Extensible Distributed Coordination must reach for stored-procedure coordination precisely where programs are non-monotonic. Contrasts with Are Multiagent Systems Resilient to Communication Failures: that paper shows game-theoretic MAS are brittle under message loss — CALM identifies the logical class of programs immune to such loss. The monotonic/non-monotonic split echoes Foundations of Logic Programming - Lloyd’s distinction between Horn-clause logic and Negation as Failure.

Gossip Protocols

Epidemic information dissemination and aggregation in distributed systems.

Sources

Distributed Snapshots Determining Global States of Distributed Systems

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.