Eventual Consistency

Chapter 1: The Consistency Spectrum

Most developers think of consistency as binary: either your system is consistent or it isn't. This is like saying temperature is binary — either hot or cold. In reality, there's a precise spectrum of consistency guarantees, each one relaxing a specific constraint to gain performance or availability.

Before Burckhardt's formalization, the consistency landscape was confusing. Different papers used the same terms to mean different things. "Eventual consistency" in Amazon's Dynamo paper meant something subtly different from "eventual consistency" in Werner Vogels's blog post, which was different again from the academic definition. Burckhardt's contribution was to pin each model down with mathematical axioms, making the definitions unambiguous.

What emerged is surprisingly elegant: the models form a clean hierarchy, each one obtained from the previous by removing exactly one axiom. Understanding this hierarchy is the single most important thing you can learn about distributed systems — it's the map that tells you exactly what you're getting and what you're giving up for every design choice you make.

Burckhardt's key insight is that each consistency model is a set of axioms about how operations relate to each other. Stronger models have more axioms. Weaker models have fewer. Fewer axioms means more behaviors are "legal" — which means the system has more freedom, which means it can be faster and more available, but also harder for programmers to reason about.

The Hierarchy

From strongest to weakest:

Linearizability (the gold standard). Every operation appears to take effect at a single instant between its invocation and completion. All observers see operations in the same order, and that order respects real-time. If operation A finishes before operation B starts, then A appears before B — for everyone. This is what single-threaded programs give you for free. In a distributed system, it requires coordination on every operation.

Sequential consistency. There exists SOME total order of all operations that is consistent with each client's local order. But this order does NOT have to respect real-time. If you write X=1, then I write X=2, a sequentially consistent system could show everyone X=1 (ordering my write before yours), as long as each individual client's operations appear in the order they issued them. The difference from linearizability: real-time ordering is not preserved across clients.

Causal consistency. If operation A could have influenced operation B (because B happened after A on the same client, or B read a value written by A), then everyone sees A before B. But operations that are concurrent — neither could have influenced the other — may appear in different orders on different replicas. This is weaker than sequential because there's no single total order of concurrent operations.

Eventual consistency. If no new updates are made, all replicas will eventually converge to the same value. That's it. No ordering guarantees during updates. No bound on how long "eventually" takes. Replicas can temporarily disagree on everything. The only promise: silence leads to agreement.

Quiescent consistency. Even weaker — convergence is only guaranteed during periods of quiescence (no operations in flight). If operations never stop, replicas may never converge. This is the absolute floor of useful consistency.

Worked Example: What Each Model Allows

Two clients, two replicas. Client A writes X=1, then Client B writes X=2. Client C reads X from both replicas.

Linearizability: The Gold Standard (In Detail)

Linearizability deserves special attention because it's what single-threaded programs give you for free — and what distributed systems spend enormous effort to approximate. The formal definition: every operation appears to take effect at a single, atomic point between its invocation and completion, and all operations are consistent with a single global total order that respects real time.

Checking whether an execution history is linearizable is NP-complete in general (you're searching for a linearization point assignment). In practice, tools like Jepsen use randomized testing to find violations.

Causal Consistency: The Sweet Spot

Many practitioners argue that causal consistency is the "sweet spot" — it prevents the most confusing anomalies (seeing a reply before the original message) while remaining implementable without global coordination. The key: causal consistency requires no total order of concurrent operations, which means replicas don't need to agree on how to order unrelated events.

Chapter 2: Event Graphs & Histories

To reason precisely about consistency, we need precise language. Without formalism, engineers argue in circles: "our system is eventually consistent" — but what does that MEAN? When does it converge? What can a reader see during convergence? What ordering is guaranteed? These questions have precise answers, but only if we define our terms precisely.

Burckhardt's formalism starts with the simplest possible building block: an event. Every time a client reads or writes a value, that's an event. An event has an operation (what it did), a return value (what it saw), and an identity (which client, when, where). Events are the atoms of distributed computation — everything else is built from them.

The genius of this approach is its generality. Whether you're building a key-value store, a message queue, a file system, or a collaborative editor, the formal model is the same: events, visibility, session order, arbitration. The specific operations differ, but the framework for reasoning about consistency is universal.

Now the key question: which events can "see" other events? If event A writes X=5 and event B later reads X=5 on the same replica, then B can see A. We write this as A vis B — "A is visible to B." But if B is on a different replica and the write hasn't propagated yet, A is NOT visible to B. B might read an old value, or nothing.

The visibility relation is the formal way of saying "this operation knew about that operation." It captures the flow of information through the system. When you replicate a write from node A to node B, you're extending the visibility relation: events on A become visible to future events on B. The strength of a consistency model is determined by how much visibility it guarantees.

The Three Relations

Session order (so). Events by the same client are ordered. If client 1 writes X, then reads Y, the write comes before the read in session order. This is the programmer's expectation: my operations happen in the order I issued them.

Visibility (vis). Which events can an operation "see"? If event A is visible to event B, then B's return value was computed with knowledge of A. Visibility is NOT the same as session order — an event on replica 2 might see events from replica 1 (after replication), but session order only relates events from the same client.

Arbitration (ar). A total order on events that resolves conflicts. When two events write to the same key, arbitration decides who "wins." Think of it as the tiebreaker. In a last-writer-wins register, arbitration is determined by timestamps. In a Paxos-based system, arbitration is the consensus order.

A History

These three relations — session order, visibility, and arbitration — are the alphabet of Burckhardt's formalism. Every consistency guarantee, every protocol property, every correctness proof is written in terms of these relations. Master them, and the rest of the framework follows.

Formally, a history is a tuple H = (E, op, rval, so, vis) where:

Happens-Before: Combining Session Order and Visibility

Lamport's famous happens-before relation is the transitive closure of session order and visibility combined. If A is in session order before B, and B is visible to C, then A happens before C — even though A and C might be on different clients and different replicas.

Two events are concurrent if neither happens before the other:

Concurrent events are the root of all distributed systems complexity. If two events are ordered by happens-before, we know which one "came first" and can resolve conflicts. If they're concurrent, there IS no "first" — both happened independently, and the system must have a strategy for resolving the disagreement.

Happens-Before is NOT Wall-Clock Time

A critical distinction. Wall-clock time (UTC timestamps) is NOT the same as happens-before ordering. Two events can happen at the same wall-clock time on different replicas and still be ordered by happens-before (if one saw the other via replication). Conversely, two events with different wall-clock times can be concurrent (if neither saw the other).

This is why Lamport invented logical clocks — to capture happens-before without relying on physical time. Vector clocks extend this to capture exactly which events each replica has seen, enabling precise concurrency detection.

Worked Example: Building an Event Graph

Chapter 3: Abstract Executions & Consistency Guarantees

We have events, visibility, session order, and arbitration. Now Burckhardt's central contribution: a consistency guarantee is a SET OF AXIOMS constraining these relations. Each axiom forbids certain behaviors. More axioms = stronger consistency = fewer legal executions = harder to implement efficiently.

An abstract execution is a tuple A = (H, vis, ar) where H is a history, vis is the visibility relation, and ar is the arbitration (total conflict-resolving order). A consistency model is a predicate that says "this abstract execution is legal" or "this one is not."

The Axioms

Burckhardt identifies five core axioms. Every consistency model is a combination of these:

Axiom 1: Eventual Visibility (EVIS). For any two events a and b, eventually a becomes visible to b or b becomes visible to a. No event stays invisible forever.

Axiom 2: Consistent Visibility (CVIS). Visibility is consistent with session order. If a client does operation A then operation B, anything visible to A is also visible to B.

In other words: a client never "forgets" what it has seen. If you read X=5 and then read X again, you won't see X=3 (an older value). This is also called monotonic reads.

Axiom 3: Consistent Arbitration (CAR). Arbitration is consistent with visibility. If a is visible to b, then a comes before b in the arbitration order.

Axiom 4: Total Visibility (TVIS). If b sees a, then b sees everything that a saw. Visibility is transitively closed.

Axiom 5: Real-Time Order (RTO). If operation a completes before operation b starts (in wall-clock time), then a is visible to b.

Building Models from Axioms

Why Axioms, Not Algorithms?

You might wonder: why define consistency models as axioms instead of algorithms? Because the same consistency guarantee can be implemented by many different protocols. Linearizability can be achieved by Paxos, Raft, viewstamped replication, or a single-node database. By defining models as axioms on abstract relations, Burckhardt separates the WHAT (the guarantee) from the HOW (the implementation). This lets you prove that a new protocol provides a known guarantee, or that a known guarantee is sufficient for your application — independently.

It's the same principle as interfaces in programming: the axioms are the interface, the protocols are the implementations. You can swap implementations without changing the guarantee, and you can analyze the guarantee without knowing the implementation.

The Axiom Dependencies

The axioms are not independent — some imply others, and some combinations are contradictory or redundant. Understanding the dependency structure is key to navigating the consistency hierarchy:

Worked Example: Which Executions Are Legal?

Counting Legal Executions: A Complexity Perspective

Here's an eye-opening way to understand the consistency spectrum: count how many distinct executions are legal under each model for the same set of operations.

This is why eventual consistency is hard for programmers. If you write code that reads a value and branches on it, under linearizability there's one possible execution path. Under eventual consistency, there could be many. Your code must handle ALL of them correctly.

Chapter 4: Replicated Data Types (CRDTs)

Abstract executions and axioms tell us what guarantees a system provides. But they don't tell us HOW to build it. We need data structures that can live on multiple replicas, accept updates independently, and converge to the same state without coordination. These are Conflict-free Replicated Data Types — CRDTs.

The idea is deceptively simple, and the name is slightly misleading. "Conflict-free" doesn't mean conflicts don't happen — it means conflicts are resolved automatically, without human intervention, using mathematical properties of the data structure. A better name might be "automatically-convergent replicated data types," but CRDT is catchier.

A sequential data type is what you already know: a set of states, a set of operations, and a specification mapping (state, operation) to (new state, return value). A stack, a counter, a register, a set — all sequential data types. You interact with them one operation at a time, and each operation sees the result of all previous operations.

A replicated data type extends this to handle concurrent operations on multiple replicas. The question is: when two replicas independently apply different operations and then sync, do they end up in the same state? If YES for all possible orderings of all possible operations, the data type is a CRDT.

This is a remarkably strong guarantee. It says that NO matter what operations happen, in what order, on which replicas, with what delays or duplications in message delivery — the final state is ALWAYS the same. This is what "conflict-free" means: not that conflicts don't occur, but that they resolve themselves deterministically.

Three CRDT Families

State-based CRDTs (CvRDTs). Each replica maintains a complete copy of the state. Replicas periodically send their entire state to other replicas, which merge the received state with their own. The merge function must be commutative, associative, and idempotent — in other words, it must form a join-semilattice.

Operation-based CRDTs (CmRDTs). Instead of sending full states, replicas broadcast operations. The key requirement: operations must commute. If replica A applies op1 then op2, and replica B applies op2 then op1, both must end up in the same state. This needs a reliable broadcast layer (every operation delivered at least once to every replica).

Delta-based CRDTs. A hybrid. Instead of full states (expensive for large data) or operations (need reliable broadcast), send only the DELTA — the part of the state that changed. Deltas must also form a join-semilattice. This is what modern implementations like Riak and Akka Distributed Data use.

The Convergence Theorem

Burckhardt's formal statement: a state-based CRDT with a join-semilattice merge function, where update operations are monotonically increasing (the state only moves "up" in the lattice), converges to a least upper bound under eventual delivery.

What IS a Join-Semilattice? (Concretely)

This sounds abstract, but it's just a fancy name for a set with a "combine" operation that always produces the same result regardless of order. Think of it like a bag of marbles: if you pour bag A into bag B, or bag B into bag A, you get the same combined bag. And pouring a bag into itself changes nothing.

Formally, a join-semilattice is a set S with a partial order ≤ and a binary operation ⊔ (join) such that for any a, b in S, a ⊔ b is the least upper bound — the smallest element that's greater than or equal to both a and b.

Formal Proof: G-Counter Forms a Join-Semilattice

Let's prove rigorously that the G-Counter merge function satisfies all three semilattice properties. This is the kind of proof Burckhardt demands — not handwaving, but step-by-step verification.

This proof may seem trivially simple — and it is, for the G-Counter. But when you get to more complex CRDTs like OR-Sets or RGA (Replicated Growable Arrays for text editing), the proofs become intricate. The G-Counter is the "hello world" of CRDT proofs: simple enough to understand, complex enough to illustrate the technique.

State Size vs. Message Size: The Delta Trade-off

State-based CRDTs send the entire state on every sync. For a G-Counter with 100 replicas, that's 100 integers — fine. For an OR-Set with 10 million entries, sending the full state is catastrophic. This is where delta-based CRDTs shine.

A delta-CRDT only sends the change since the last sync. The key requirement: deltas must also form a semilattice, so they can be merged independently. The receiver accumulates deltas and periodically merges them into its full state. If deltas are lost, the sender falls back to sending the full state — but this is rare.

Chapter 5: Counters & Registers

Let's implement the fundamental CRDTs from scratch. Each one follows the same pattern: define the state, define the update operations, define the merge function, prove convergence. This is the "concept to realization" bridge — by the end of this chapter, you'll be able to implement any of these from memory.

We start with the simplest (G-Counter) and build toward the most complex (MV-Register). Each builds on the previous: the PN-Counter uses two G-Counters, the LWW-Register uses timestamps like the G-Counter uses max, and the MV-Register uses version vectors — which are themselves G-Counters used for tracking causality rather than counting.

G-Counter (Grow-only Counter)

The simplest useful CRDT, and arguably the most important — because it demonstrates the core principle that all CRDTs share. Each of N replicas maintains a vector of N integers. Replica i only increments position i. The counter value is the sum of all positions. Merge is component-wise maximum.

Why a vector instead of a single integer? Because we need the merge function to be idempotent. If we used addition, merging the same state twice would double the count. With max, merging the same state twice changes nothing — which is exactly what idempotency requires.

Worked Trace: G-Counter with 3 Replicas

PN-Counter (Positive-Negative Counter)

G-Counters can only go up. What if you need decrements? The naive approach — allowing negative values in the vector — breaks the semilattice property (max of -3 and 5 is 5, but that loses the -3 decrement). The elegant solution: use TWO G-Counters. One for increments (P), one for decrements (N). The value is P.value() - N.value(). Each G-Counter independently satisfies the semilattice properties, and subtraction preserves the correct total.

This "decompose into monotonic components" pattern appears throughout CRDT design. When you need a non-monotonic operation (decrement, remove), split the state into monotonically increasing parts and derive the non-monotonic result from them.

PN-Counter: Full Worked Trace with Concurrent Decrements

LWW-Register (Last-Writer-Wins Register)

A register holds a single value. When two replicas write concurrently, who wins? The LWW-Register uses timestamps: the write with the highest timestamp wins. Simple, but lossy — concurrent writes are silently discarded. Despite its simplicity, LWW is one of the most widely deployed CRDTs — Cassandra uses it for every cell in every table by default.

The catch: LWW requires globally unique, monotonically increasing timestamps. In a distributed system, clock skew means two replicas might assign the same timestamp to different writes. Worse, a replica with a fast clock will always "win" over a replica with a slow clock, regardless of actual event ordering. This is why systems like Cassandra use hybrid logical clocks — combining physical time with a logical counter to guarantee uniqueness.

MV-Register (Multi-Value Register)

The alternative to LWW: keep ALL concurrent values and let the application resolve the conflict. This is the MV-Register (Multi-Value Register). Amazon's original Dynamo shopping cart used this approach — concurrent adds to a shopping cart produce a set of carts, which the application merges (usually: union of all items).

The MV-Register uses version vectors (essentially vector clocks for data versions) to detect concurrency. When two writes have incomparable version vectors (neither dominates the other), they're concurrent, and both values are kept. When a later write has a version vector that dominates an earlier one, the earlier value is replaced.

MV-Register: Detailed Worked Trace

Python Implementations

python
class GCounter:
    """Grow-only counter CRDT."""
    def __init__(self, node_id, n_nodes):
        self.id = node_id
        self.vector = [0] * n_nodes

    def increment(self):
        self.vector[self.id] += 1

    def value(self):
        return sum(self.vector)

    def merge(self, other):
        for i in range(len(self.vector)):
            self.vector[i] = max(self.vector[i], other.vector[i])


class PNCounter:
    """Positive-Negative counter = two G-Counters."""
    def __init__(self, node_id, n_nodes):
        self.P = GCounter(node_id, n_nodes)
        self.N = GCounter(node_id, n_nodes)

    def increment(self):
        self.P.increment()

    def decrement(self):
        self.N.increment()

    def value(self):
        return self.P.value() - self.N.value()

    def merge(self, other):
        self.P.merge(other.P)
        self.N.merge(other.N)


class LWWRegister:
    """Last-Writer-Wins Register."""
    def __init__(self):
        self.value = None
        self.timestamp = 0

    def write(self, val, ts):
        if ts > self.timestamp:
            self.value = val
            self.timestamp = ts

    def read(self):
        return self.value

    def merge(self, other):
        if other.timestamp > self.timestamp:
            self.value = other.value
            self.timestamp = other.timestamp


class MVRegister:
    """Multi-Value Register — keeps all concurrent values."""
    def __init__(self, node_id, n_nodes):
        self.id = node_id
        self.n = n_nodes
        self.entries = []  # list of (value, vector_clock)
        self.clock = [0] * n_nodes

    def write(self, val):
        self.clock[self.id] += 1
        # New write dominates all current entries
        self.entries = [(val, self.clock[:])]

    def read(self):
        return [v for v, _ in self.entries]

    def _dominates(self, vc1, vc2):
        """Does vc1 causally dominate vc2?"""
        return (all(vc1[i] >= vc2[i] for i in range(self.n))
                and vc1 != vc2)

    def merge(self, other):
        # Combine entries, keep only non-dominated ones
        all_entries = self.entries + other.entries
        kept = []
        for v, vc in all_entries:
            dominated = any(
                self._dominates(vc2, vc)
                for _, vc2 in all_entries
            )
            if not dominated:
                kept.append((v, vc))
        # Deduplicate by vector clock
        seen = set()
        self.entries = []
        for v, vc in kept:
            key = tuple(vc)
            if key not in seen:
                seen.add(key)
                self.entries.append((v, vc))
        # Merge clocks
        for i in range(self.n):
            self.clock[i] = max(self.clock[i], other.clock[i])


# Demo: MV-Register concurrent writes
r0 = MVRegister(0, 3)
r1 = MVRegister(1, 3)
r0.write("Alice")          # r0: [("Alice", [1,0,0])]
r1.write("Bob")            # r1: [("Bob", [0,1,0])]
r0.merge(r1)
print(r0.read())           # ["Alice", "Bob"] — concurrent!
r0.write("Carol")          # resolves conflict
print(r0.read())           # ["Carol"] — single value

Chapter 6: Sets & Maps

Counters and registers handle single values. Most real applications need collections: shopping carts (sets of items), user permissions (sets of roles), configuration maps (key-value pairs). Making these conflict-free is harder than you'd think, because collections have an operation that counters and registers don't: remove. And remove in a distributed system is surprisingly tricky — when you remove an element that was concurrently added on another replica, which one wins?

G-Set (Grow-only Set)

The simplest collection CRDT: you can add elements but never remove them. Merge is union.

This is trivially a CRDT — union is commutative, associative, and idempotent. But it's rarely useful in practice. You almost always need to remove elements.

G-Set: Worked Trace

G-Sets are perfect for tracking "have I seen this before?" — duplicate detection, read receipts, visited URLs. Anything where you only need to add elements and never remove them.

2P-Set (Two-Phase Set)

Like the PN-Counter pattern: two G-Sets, one for adds (A) and one for removes (R). An element is in the set if it's in A but NOT in R. The catch: once an element is removed, it can NEVER be re-added (it's permanently in R).

OR-Set (Observed-Remove Set) — The Practical CRDT

The OR-Set is the most important set CRDT. The key idea: each ADD generates a unique tag. When you REMOVE an element, you only remove the tags you've OBSERVED — tags you haven't seen (from concurrent adds on other replicas) survive.

Formally: the state is a set of (element, unique-tag) pairs. Add(e) inserts (e, fresh_tag). Remove(e) removes all pairs (e, *) currently visible on this replica. Merge is union of all pairs.

Why "Observed-Remove" Matters: A Shopping Cart Example

Consider Amazon's shopping cart, one of the most famous eventual-consistency use cases. You add milk to your cart on your phone. Your partner removes milk from the cart on their laptop. Concurrently, you add milk again (you realized you need two cartons). With a 2P-Set, the re-add fails — milk is in the tombstone set forever. With an OR-Set, the re-add generates a fresh tag, B's remove only killed the tags it observed, and the fresh tag survives. Milk is in the cart.

Amazon's original Dynamo paper (2007) used a similar approach: the shopping cart was an MV-Register that kept concurrent versions. The application merged them by taking the union of all items. This occasionally produced "resurrected" items (items that were removed would reappear), which Amazon preferred over lost items. The OR-Set formalizes this: add always wins over concurrent remove.

The Full OR-Set Merge (with tombstone optimization)

The naive OR-Set keeps growing forever — removed tags are gone from the local set but might arrive again via a stale replica. The practical fix: maintain a causal context (a vector clock summarizing all tags seen) alongside the entries. During merge, any tag that's in the causal context but NOT in the entries was explicitly removed.

Python OR-Set Implementation

python
import uuid

class ORSet:
    """Observed-Remove Set CRDT. Add-wins semantics."""
    def __init__(self):
        self.entries = set()  # set of (element, unique_tag) tuples

    def add(self, element):
        tag = str(uuid.uuid4())[:8]
        self.entries.add((element, tag))

    def remove(self, element):
        # Remove only the tags we can SEE right now
        observed = {(e, t) for e, t in self.entries if e == element}
        self.entries -= observed

    def lookup(self, element):
        return any(e == element for e, _ in self.entries)

    def elements(self):
        return {e for e, _ in self.entries}

    def merge(self, other):
        # Union of all (element, tag) pairs.
        # Tags removed on one side but present on the other
        # survive — that's the "add-wins" behavior.
        self.entries = self.entries | other.entries


# Demo: concurrent add and remove
a = ORSet()
b = ORSet()
a.add("milk")
b.merge(a)       # b sees "milk"
b.remove("milk")  # b removes observed tags
a.add("milk")     # a concurrently re-adds with NEW tag
a.merge(b)
b.merge(a)
print(a.lookup("milk"))  # True — concurrent add survived
print(b.lookup("milk"))  # True — converged

OR-Set: Why "Add-Wins" is the Right Default

The OR-Set's "add-wins" semantics might seem arbitrary. Why should add beat remove? Consider the alternative: "remove-wins" (if anyone removes X concurrently with someone adding X, X is removed). This is actually worse for most applications:

This principle — prefer not losing data — is why most CRDT designs bias toward preservation. It's the same philosophy behind Git's merge conflicts: show both versions and let the human decide, rather than silently picking one.

Vector Clocks for Version Tracking

The MV-Register and OR-Set both need to track causality — "which events has this replica seen?" The standard tool is a vector clock: each replica maintains a vector of N counters, one per replica. When replica i does an operation, it increments V[i]. When it receives a message from replica j with vector V', it sets V[k] = max(V[k], V'[k]) for all k.

python
class VectorClock:
    """Tracks causality across N replicas."""
    def __init__(self, node_id, n_nodes):
        self.id = node_id
        self.clock = [0] * n_nodes

    def tick(self):
        """Local event: increment own counter."""
        self.clock[self.id] += 1

    def merge(self, other_clock):
        """Merge with received clock."""
        for i in range(len(self.clock)):
            self.clock[i] = max(self.clock[i], other_clock[i])
        self.clock[self.id] += 1  # receiving is also an event

    def dominates(self, other):
        """Does self causally dominate other?"""
        return (all(self.clock[i] >= other.clock[i]
                    for i in range(len(self.clock)))
                and self.clock != other.clock)

    def concurrent(self, other):
        """Are self and other concurrent?"""
        return not self.dominates(other) and not other.dominates(self)

Chapter 7: Consistency Models — The Showcase

This is the payoff chapter. Everything we've learned — event graphs, axioms, CRDTs — converges in one interactive simulation. You control a distributed system with three replicas. You perform read/write operations on any replica. And you toggle between consistency models to see exactly which read results are legal under each one.

If you can predict what each model allows before clicking "Read All" — then you've internalized the formal framework. Every consistency debate in a design review reduces to this: "which behaviors does our model allow, and can our application tolerate them?"

The insight that makes distributed systems engineering hard is not that eventual consistency exists. It's that you can't tell the difference between consistency models during normal operation. When the network is fast and healthy, linearizable and eventual consistency look identical. The difference only manifests during partitions, lag, and concurrent access. This simulation forces those edge cases so you can see what each model actually guarantees.

How To Use This Simulator

Here's a specific experiment to try. Follow these steps exactly:

The visual difference is striking. Under eventual consistency, each replica lives in its own world. Under linearizability, there's one global truth. Every level in between is a different blend of "local truth" vs "global truth."

What You Should Observe

The Mental Model

Think of consistency models as constraints on a jigsaw puzzle. Linearizability says there's exactly one way to assemble the pieces — the real-time order. Sequential says any assembly that respects each person's piece order is fine. Causal says pieces that were placed "because of" earlier pieces must keep that order, but unrelated pieces can go anywhere. Eventual says you can scatter pieces across the table — as long as you eventually put them all together, the final picture will be the same for everyone.

The programmer's job is to choose the weakest model that still makes the application correct. Weaker models are faster and more available. The art is knowing what anomalies your application can tolerate.

Anomaly Catalog: What Goes Wrong at Each Level

Each weakening of the consistency model introduces specific anomalies. Understanding these anomalies is how you choose the right model for your application.

The Decision Framework

Worked Example: Choosing Consistency for a Chat App

Chapter 8: Protocol Templates

Models tell us WHAT guarantees we want. Protocols tell us HOW to achieve them. Burckhardt identifies three protocol families, each implementing a different point on the consistency spectrum. The mapping is clean: one family per level.

Understanding these protocols is critical for system design interviews. When an interviewer asks "how would you implement X," the answer is almost always one of these three patterns — or a hybrid. The choice determines your latency, availability, and programming complexity.

Each protocol can be understood as answering one question: when does a replica learn about another replica's operations? Immediately (global-sequence), when causally needed (broadcast), or eventually (epidemic). The answer determines everything about the system's behavior.

1. Epidemic (Gossip) Protocols — For Eventual Consistency

Each replica periodically picks a random partner and exchanges state. After merging, both have the same information. Over time, every update reaches every replica — like a rumor spreading through a crowd.

There are three variants of gossip: push (I send my state to you), pull (I request your state), and push-pull (we exchange states). Push-pull converges fastest because each interaction makes both parties up-to-date. Push converges in O(N log N) messages; push-pull converges in O(N log log N) — a significant improvement for large clusters.

The gossip interval (how often each node contacts a peer) creates a direct tradeoff between convergence speed and network bandwidth. Gossip every 100ms and you converge in seconds; gossip every 10 seconds and you converge in minutes. Most systems use 1-second gossip intervals, giving convergence in 5-20 seconds for clusters of 100+ nodes.

2. Broadcast Protocols — For Causal Consistency

Tag each operation with a vector clock. Deliver operations in causal order: an operation is only applied when all operations it depends on have been applied. This guarantees CVIS and TVIS axioms.

The key mechanism is the delivery buffer. When a message arrives whose dependencies aren't met yet (the sender saw events that the receiver hasn't seen), the message waits in a buffer until the missing events arrive. This buffer is what makes causal broadcast more expensive than epidemic — messages can be delayed, and the buffer can grow during bursts of activity or slow networks.

3. Global-Sequence Protocols — For Strong Consistency

A single designated node (or a consensus protocol like Paxos/Raft) assigns a global sequence number to every operation. All replicas apply operations in this sequence. This gives linearizability (with a leader) or sequential consistency (with consensus).

The fundamental cost of global-sequence protocols is the consensus round. Every write requires a majority of replicas to acknowledge before the operation is committed. This means the write latency is dominated by the slowest node in the majority — typically the one farthest away in terms of network distance. For a 3-node cluster in a single datacenter, this might be 5ms. For a 5-node cluster spanning continents, this could be 200ms.

This is why global-sequence protocols are impractical for latency-sensitive operations across geographic regions. Spanner works around this with GPS-synchronized atomic clocks (TrueTime), but this requires specialized hardware that most organizations can't afford.

Gossip Protocol: The Mathematics of Rumor Spreading

Epidemic protocols borrow directly from mathematical epidemiology. The spread of an update through a gossip network follows the same differential equation as the spread of an infectious disease through a population. This is not a metaphor — it's the same math.

Vector Clocks in Practice: The Space Problem

Causal broadcast uses vector clocks with one entry per replica. With N replicas, each message carries an N-dimensional vector. For N=5, this is trivial. For N=10,000 (a large Cassandra cluster), this is 10,000 integers per message — a serious overhead.

Global-Sequence: The Raft Example

Let's trace a write through a Raft-based global-sequence protocol. Raft is the most widely-used consensus algorithm (etcd, CockroachDB, TiKV). The key: one leader sequences all operations; followers replicate in order.

Latency Comparison: Real Numbers

Python: Complete Gossip Protocol Simulator

python
import random

class GossipNode:
    """A single node in a gossip network with a G-Counter."""
    def __init__(self, node_id, n_nodes):
        self.id = node_id
        self.counter = GCounter(node_id, n_nodes)
        self.inbox = []  # messages waiting to be processed

    def increment(self):
        self.counter.increment()

    def send_state(self):
        """Return current state to send to a random peer."""
        return self.counter.vector[:]

    def receive_state(self, remote_vector):
        """Merge received state with local state."""
        for i in range(len(self.counter.vector)):
            self.counter.vector[i] = max(
                self.counter.vector[i],
                remote_vector[i]
            )


def simulate_gossip(n_nodes=10, n_increments=20, n_rounds=50):
    """Simulate gossip convergence."""
    nodes = [GossipNode(i, n_nodes) for i in range(n_nodes)]

    # Phase 1: random increments on random nodes
    for _ in range(n_increments):
        node = random.choice(nodes)
        node.increment()

    # Phase 2: gossip rounds
    for round_num in range(n_rounds):
        # Each node contacts one random peer
        for node in nodes:
            peer = random.choice(nodes)
            if peer.id != node.id:
                state = node.send_state()
                peer.receive_state(state)

        # Check convergence
        values = [n.counter.value() for n in nodes]
        if len(set(values)) == 1:
            print(f"Converged in round {round_num}! Value: {values[0]}")
            return round_num

    print(f"Did not converge in {n_rounds} rounds.")
    return n_rounds

# Run simulation
rounds = [simulate_gossip() for _ in range(100)]
print(f"Average rounds to converge: {sum(rounds)/len(rounds):.1f}")
# Typically: 3-5 rounds for 10 nodes. O(log N) behavior.

Python: Causal Broadcast with Vector Clocks

python
class CausalBroadcastNode:
    """Node implementing causal broadcast via vector clocks."""
    def __init__(self, node_id, n_nodes):
        self.id = node_id
        self.n = n_nodes
        self.clock = [0] * n_nodes
        self.state = {}     # key-value store
        self.buffer = []    # undelivered messages
        self.delivered = []  # delivered operations log

    def write(self, key, val):
        self.clock[self.id] += 1
        self.state[key] = val
        # Return message to broadcast
        return {'op': (key, val),
                'sender': self.id,
                'vc': self.clock[:]}

    def receive(self, msg):
        """Buffer message, deliver when deps satisfied."""
        self.buffer.append(msg)
        self._try_deliver()

    def _can_deliver(self, msg):
        """Check if all causal dependencies are met."""
        vc = msg['vc']
        sender = msg['sender']
        # Sender's count must be exactly our count + 1
        if vc[sender] != self.clock[sender] + 1:
            return False
        # All other entries must be ≤ our clock
        for k in range(self.n):
            if k != sender and vc[k] > self.clock[k]:
                return False
        return True

    def _try_deliver(self):
        progress = True
        while progress:
            progress = False
            for msg in self.buffer[:]:
                if self._can_deliver(msg):
                    self.buffer.remove(msg)
                    key, val = msg['op']
                    self.state[key] = val
                    self.clock[msg['sender']] += 1
                    self.delivered.append(msg)
                    progress = True

Chapter 9: The CAP Theorem (Formally)

You've heard "pick two of three: Consistency, Availability, Partition tolerance." But what does this ACTUALLY mean? Most explanations are hand-wavy. Burckhardt gives the precise formal statement and proof. And most people who cite CAP get it wrong — either they think it means "choose any two" (it doesn't — P is not optional), or they think it applies during normal operation (it doesn't — CAP only matters during partitions), or they think it's about eventual consistency (it's not — CAP's "C" means sequential or stronger).

Getting CAP right in an interview is a differentiator. Let's build the correct understanding from the formal definitions.

Definitions (Precise)

Consistency (C): Here means specifically sequential consistency (or stronger). Every read returns a value consistent with some total order of all operations that respects each client's order. Note: this is NOT eventual consistency. CAP's "C" is the strong kind.

Availability (A): Every request to a non-failed node receives a response. Not "eventually" — within a bounded time. A system that blocks forever waiting for a partitioned node is NOT available.

Partition tolerance (P): The system continues to operate despite arbitrary message loss between nodes. Since network partitions are a fact of life (not a choice), every real distributed system must be partition-tolerant. "P" is not optional.

The Formal Proof

The proof is by contradiction, and it's beautifully simple. Assume a system that is both sequentially consistent AND available during a partition. Show that this leads to a contradiction.

What Systems Actually Choose

Beyond CAP: The PACELC Model

CAP only talks about partition scenarios. But even during normal operation, there's a tradeoff between latency and consistency. The PACELC model extends CAP:

How Google Spanner "Cheats" CAP

Google Spanner claims to be a globally-distributed, strongly-consistent, highly-available database. Doesn't this violate CAP? Technically no. Spanner is a CP system — during a partition, it sacrifices availability on the minority side. But Google has invested billions in network infrastructure to make partitions astronomically rare.

CAP is a Theorem, Not a Framework

A common mistake: treating CAP as a design framework ("I'll build an AP system"). CAP is a negative result — it tells you what's impossible, not what to build. The right way to use CAP:

Chapter 10: Correctness Proofs

Saying "my CRDT converges" is easy. Proving it requires a simulation relation between the concrete protocol execution and the abstract consistency model. This is how Burckhardt verifies that a protocol actually implements the consistency guarantees it claims.

Why should you care about correctness proofs? Because distributed systems bugs are the hardest to find. They only manifest under specific timing conditions, specific failure patterns, specific message orderings. You can test for months and miss a bug that only appears when a specific replica is 200ms behind, during a garbage collection pause, while a network switch is rebooting. Proofs catch these bugs at design time, before any code is written.

The industry learned this the hard way. Amazon's DynamoDB team discovered that their original hash ring implementation had a subtle consistency violation that only occurred during simultaneous node joins and departures. MongoDB's initial causal consistency implementation had a gap in the vector clock protocol that allowed causal ordering violations during primary elections. Both bugs were found by formal analysis, not testing.

The Proof Structure

A correctness proof has three parts:

1. Define the abstract specification. What consistency model are we targeting? For a G-Counter with epidemic protocol, the target is eventual consistency: the EVIS axiom (all events eventually visible).

2. Define the simulation relation. Map each concrete state (vector values on each replica, messages in flight) to an abstract execution (events, visibility, arbitration). The simulation relation R(concrete, abstract) says: "this concrete state corresponds to this abstract execution."

3. Prove the simulation. Show that for every step the concrete protocol takes (local update, send message, receive message, merge), the corresponding abstract execution remains legal — i.e., the axioms still hold.

Worked Proof: G-Counter + Epidemic Protocol = Eventual Consistency

Why Proofs Matter in Practice

You might think: "I'll never write a formal proof at work." True. But understanding the proof structure helps you spot bugs. The most common distributed systems bugs violate one of the proof steps:

The Engineer's Verification Checklist

You don't need to write formal proofs. But you DO need to verify these properties. Here's how to test each one in practice:

python
def test_crdt_properties(crdt_class, n_trials=1000):
    """Property-based test for CRDT correctness."""
    import random

    for _ in range(n_trials):
        # Create two replicas with random operations
        a = crdt_class(0, 3)
        b = crdt_class(1, 3)

        for _ in range(random.randint(1, 10)):
            a.increment()
        for _ in range(random.randint(1, 10)):
            b.increment()

        # Test commutativity: merge(a,b) == merge(b,a)
        ab = crdt_class(0, 3); ab.vector = a.vector[:]
        ba = crdt_class(1, 3); ba.vector = b.vector[:]
        ab.merge(b)
        ba.merge(a)
        assert ab.vector == ba.vector, "Commutativity failed!"

        # Test idempotency: merge(a,a) == a
        aa = crdt_class(0, 3); aa.vector = a.vector[:]
        aa.merge(a)
        assert aa.vector == a.vector, "Idempotency failed!"

    print("All properties verified!")

test_crdt_properties(GCounter)  # Should pass

Proof Sketch: Causal Broadcast Protocol Correctness

Let's also outline the proof for a causal broadcast protocol — this is harder than the epidemic proof because we need to verify three axioms (EVIS, CVIS, TVIS) instead of just one.

Common Implementation Bugs and How the Proof Catches Them

Chapter 11: Connections & Cheat Sheet

Mapping to DDIA

If you've studied the DDIA lessons in this series, here's how Burckhardt's formal framework maps to Kleppmann's practical treatment. Every concept in DDIA has a precise formal counterpart here.

Mapping to Algorithms

Burckhardt's framework doesn't exist in isolation — it builds on decades of theoretical computer science. Here are the algorithmic foundations that underpin each concept.

Complete CRDT Cheat Sheet

Pin this table. In a system design interview, you'll reach for it constantly. Each CRDT solves a specific class of conflict — choosing the right one is half the design.

Consistency Models Cheat Sheet

The definitive reference. Each model is a precise set of axioms — not a marketing term, not a vague promise, but a mathematical specification with provable properties.

When to Use What: The Interview Decision Tree

Burckhardt's Lasting Impact

This monograph, published in 2014, laid the formal groundwork that the distributed systems community has built on for a decade. Before Burckhardt, "eventual consistency" was an informal promise. After, it became a precise mathematical property with provable implementations. The CRDT taxonomy he formalized (state-based, operation-based, delta-based) became the standard vocabulary. His axiom-based consistency hierarchy influenced the design of systems from Azure Cosmos DB to Redis CRDTs.

The key meta-insight: distributed consistency is not one problem — it's a SPECTRUM of problems, each solvable with known techniques. The engineer's job is to identify where on the spectrum each piece of data lives, and apply the right tool. Most real systems don't live at a single point on the spectrum — they use different consistency levels for different data, chosen based on the correctness requirements and performance constraints of each piece.

When you hear "we use eventual consistency" in an interview or design review, the right follow-up is: "for which data, and what conflict resolution strategy?" The answer reveals whether the speaker truly understands the system they're building.

Related Lessons

Interview Masterclass: The Five Most Common Distributed Consistency Questions

These are the questions that separate senior engineers from juniors in system design interviews. Each one maps directly to a concept from this lesson.

The Cost of Consistency: Real Latency Numbers

For replication fundamentals: DDIA Chapter 6: Database Replication

Recommended Reading

If this lesson sparked your interest, here are the primary sources. Each paper/book is foundational — they're the papers that everyone in distributed systems has read.

Real-World CRDT Deployments

The Frontier: New CRDT Research (2020-2024)

The CRDT field has exploded since Burckhardt's 2014 monograph. Key developments:

CRDT Limitations: When NOT to Use Them

CRDTs are powerful, but they are not a universal solution. Understanding when they break down is as important as knowing how they work.

The rule of thumb: CRDTs are for data where "all concurrent operations should be applied" is the right semantics. Counters (count everything), sets (add everything), text (keep all edits). They are NOT for data where operations must be mutually exclusive (seat booking, account overdraft protection).