Consistency models and the CAP theorem

Lesson 6 described how replicas exchange updates. This lesson asks what a client can observe as a result. When a client writes a value and then reads it back, from the same or a different replica, what values may the read return? When two clients write concurrently, in what order do other clients see their writes? A consistency model is a contract between a data store and its clients that answers such questions. Stronger models make programs easier to write, because the store behaves more like a single copy; weaker models allow faster, more available implementations. Choosing a model is one of the main design decisions in a distributed system, and the CAP theorem explains why the strongest models cannot be fully available during network partitions.

Linearizability

The strongest common model for a single object is linearizability, defined by Maurice Herlihy and Jeannette Wing in 1990. A history of operations is linearizable if each operation appears to take effect atomically at some instant between its invocation and its response, and the resulting order is consistent with what each operation returned. Informally, the store behaves as though there were a single copy of the data and each operation happened instantaneously at some point while it was running. Two consequences follow. Once a write has completed, every later read, by anyone, returns that value or a newer one. And once any read has returned a new value, no later read may return the old one, even from a different replica.

Linearizability is a property of real time: if operation a completes before operation b begins, a must appear before b. Operations that overlap in time may be ordered either way. The checker below tries every order of a small history and tests both conditions.

# A brute-force linearizability checker for a single register.
# Each operation: (client, kind, value, start, end). A history is linearizable if some
# order of the operations respects real time (if a ends before b starts, a comes first)
# and makes every read return the most recent write in that order.
from itertools import permutations

def linearizable(history, initial=0):
    for order in permutations(history):
        pos = {op: i for i, op in enumerate(order)}
        if any(a[4] < b[3] and pos[a] > pos[b] for a in history for b in history):
            continue                                  # violates real-time order
        val, ok = initial, True
        for c, kind, v, s, e in order:
            if kind == "write":
                val = v
            elif v != val:
                ok = False; break
        if ok:
            return True, [f"{c}:{k}({v})" for c, k, v, s, e in order]
    return False, None

H1 = [("A", "write", 1, 0, 4), ("B", "read", 1, 2, 6), ("C", "read", 0, 1, 3)]
H2 = [("A", "write", 1, 0, 2), ("B", "read", 1, 3, 4), ("C", "read", 0, 5, 6)]
H3 = [("A", "write", 1, 0, 2), ("B", "write", 2, 1, 3), ("C", "read", 2, 4, 5), ("D", "read", 1, 6, 7)]
for name, h in (("H1", H1), ("H2", H2), ("H3", H3)):
    ok, order = linearizable(h)
    print(name, "linearizable" if ok else "NOT linearizable", order or "")

H1 linearizable ['C:read(0)', 'A:write(1)', 'B:read(1)']
H2 NOT linearizable 
H3 NOT linearizable

In H1, client C's read of 0 overlaps the write, so it can be placed before the write takes effect, and B's read of 1 after it. In H2, the write has completed and B has already read 1 before C begins, so C's read of 0 sees the past: a stale read, forbidden by linearizability. In H3, two writes overlap, so either may be placed first, but once C reads 2 the later read by D of 1 would require the value to go back in time. Checking linearizability exactly is NP-complete in general, which is why practical checkers such as Knossos and Porcupine, used by Jepsen, rely on clever search and pruning.

Linearizability is what most programmers implicitly expect, and some tasks require it: a lock or leader lease must be linearizable, or two clients could both believe they hold it; a uniqueness constraint, such as one username per account, needs a linearizable check; and Ledgerline's rule that a balance never goes negative needs every withdrawal to see every earlier one. The price is coordination. A linearizable store must ensure a read sees every completed write, which typically means routing operations through a leader that confirms it is still leader, or contacting a majority of replicas, on every operation.

Sequential and causal consistency

Sequential consistency, defined by Lamport in 1979 for multiprocessor memory, requires that all operations appear in some single total order that respects each client's own program order, but not real time across clients. A client may read a stale value, provided every client sees the operations in the same order. Causal consistency is weaker still: it requires only that operations related by happened-before (lesson 3) be seen in that order by every client, while concurrent operations may be seen in different orders by different clients. If Alice posts a question and Bob replies after reading it, no one may see the reply without the question; but two unrelated posts may appear in different orders to different readers. Causal consistency is attractive because it is the strongest model that can remain available during partitions, as shown by Mahajan, Alvisi and Dahlin in 2011, and it matches much of what users care about.

Eventual consistency and session guarantees

Eventual consistency, popularized by Werner Vogels of Amazon in 2008, promises only that if updates stop, all replicas eventually converge to the same value. It says nothing about what reads return in the meantime, and nothing about how long "eventually" is. It is a liveness property with no safety component, which makes it easy to implement but hard to program against. Most eventually consistent stores offer stronger guarantees in practice, and four session guarantees, defined by Terry and colleagues for the Bayou system in 1994, describe what a single client can rely on.

Consistency for transactions

Linearizability concerns single operations on single objects. For transactions over several objects, the classic correctness criterion is serializability (CMPUT-291, lesson 10): the result is the same as if transactions ran one at a time in some order. Serializability says nothing about real time; a serializable database could, in principle, order a transaction that started later before one that committed earlier. Strict serializability combines the two: transactions appear to run one at a time in an order consistent with real time. Spanner provides strict serializability, which Google calls external consistency, using TrueTime and commit wait. Many databases default to weaker isolation levels, such as snapshot isolation or read committed, that permit anomalies like write skew, so the words "consistent" and "ACID" on a product page tell you little without the precise model.

The CAP theorem

In 2000, Eric Brewer conjectured that a distributed data store cannot simultaneously guarantee consistency, availability and tolerance of network partitions. Seth Gilbert and Nancy Lynch proved a precise version in 2002. In their formulation, consistency means linearizability; availability means every request received by a non-failed node eventually gets a non-error response; and partition tolerance means the system keeps operating although the network may lose arbitrarily many messages between nodes. The theorem says that when a partition occurs, a system must give up either linearizability or availability.

The proof idea is simple. Suppose the replicas are split into two groups that cannot communicate. A client writes a new value to a node in one group, and then another client reads from a node in the other group. To be available, the second node must answer; it cannot have learned of the write, so it returns the old value, violating linearizability. To be linearizable, it must refuse or wait until the partition heals, violating availability. No design escapes this choice.

CAP is often misquoted as "pick two of three", which is misleading. Partitions are not optional: in a real network they happen, so the real choice is what to do when they do. Systems that choose consistency, called CP, refuse some requests during a partition, typically on the minority side; consensus-based stores such as etcd, ZooKeeper and Spanner are CP. Systems that choose availability, called AP, keep answering on both sides and reconcile afterwards; Dynamo-style stores in their default configurations and DNS are AP. Brewer himself wrote in 2012 that the choice can be made per operation and per data item, and that designers should plan how to detect partitions and recover from them. Note too that CAP's availability is a strong, total notion: a CP system that keeps the majority side working is still highly available in the everyday sense.

PACELC: latency in normal operation

CAP says nothing about the much more common situation in which there is no partition. Daniel Abadi observed in 2010, and formalized in 2012 as PACELC, that even then there is a trade-off: if there is a Partition, choose Availability or Consistency; Else, choose Latency or Consistency. Strong consistency requires coordination between replicas on every operation, and coordination costs round trips, which can be tens of milliseconds between regions. A system that returns a local replica's value immediately is faster but may return stale data. Cassandra and DynamoDB with default settings are PA/EL; Spanner and etcd are PC/EC; some systems, such as MongoDB with certain settings, are PA/EC or PC/EL. For Ledgerline, PACELC frames the real decision: balances need PC/EC, paying a few milliseconds of coordination on every write within a region, while the reporting dashboards can use PA/EL replicas that may lag by seconds.

Conflict-free replicated data types

If an AP system lets replicas accept writes independently, it must merge their states when they reconnect. For some data types the merge can be made automatic, deterministic and free of conflicts. Conflict-free replicated data types (CRDTs), formalized by Marc Shapiro and colleagues in 2011, are data structures whose replicas can be updated independently and merged in any order, any number of times, always converging to the same state. A state-based CRDT achieves this by making the merge function commutative, associative and idempotent, so the replica states form a join semilattice; any two replicas that have received the same updates, in whatever order and with whatever duplication, reach the same state. This property is called strong eventual consistency.

The simplest example is a grow-only counter. Each replica keeps a vector of per-replica counts, increments only its own entry, and merges by taking the element-wise maximum, exactly like a vector clock. Its value is the sum. A counter that also decrements uses two grow-only counters, one for increments and one for decrements. Sets are harder because add and remove do not commute: if one replica removes an element while another concurrently adds it, which wins? The observed-remove set gives each add a unique tag; a remove deletes only the tags it has observed, so a concurrent add, with a tag the remover never saw, survives.

# Conflict-free replicated data types: state-based counters and an observed-remove set.
class GCounter:                                  # grow-only counter
    def __init__(self, me, n): self.me, self.p = me, [0] * n
    def inc(self, k=1): self.p[self.me] += k
    def value(self): return sum(self.p)
    def merge(self, o): self.p = [max(a, b) for a, b in zip(self.p, o.p)]

class PNCounter:                                 # increments and decrements
    def __init__(self, me, n): self.P, self.N = GCounter(me, n), GCounter(me, n)
    def inc(self, k=1): self.P.inc(k)
    def dec(self, k=1): self.N.inc(k)
    def value(self): return self.P.value() - self.N.value()
    def merge(self, o): self.P.merge(o.P); self.N.merge(o.N)

class ORSet:                                     # observed-remove set: add wins over concurrent remove
    def __init__(self, me): self.me, self.adds, self.removes, self.n = me, set(), set(), 0
    def add(self, x):
        self.n += 1; self.adds.add((x, f"{self.me}{self.n}"))      # unique tag per add
    def remove(self, x):
        self.removes |= {t for t in self.adds if t[0] == x}       # remove only tags seen
    def value(self): return sorted({x for x, tag in self.adds - self.removes})
    def merge(self, o): self.adds |= o.adds; self.removes |= o.removes

# Two replicas count invoice views while disconnected, then merge in either order.
a, b = PNCounter(0, 2), PNCounter(1, 2)
a.inc(5); b.inc(3); b.dec(1)
a2, b2 = PNCounter(0, 2), PNCounter(1, 2)
for x, y in ((a2, a), (b2, b)): x.P.p, x.N.p = y.P.p[:], y.N.p[:]
a.merge(b); b2.merge(a2)
print("counter after merge, both orders:", a.value(), b2.value())

# Tags on a draft invoice: replica X removes "urgent" while replica Y concurrently re-adds it.
x, y = ORSet("x"), ORSet("y")
x.add("urgent"); y.merge(x)                      # both start with {"urgent"}
x.remove("urgent")                               # X removes the tag it has seen
y.add("urgent"); y.add("q3")                     # Y adds it again (new tag) and adds "q3"
x.merge(y); y.merge(x)
print("OR-set after merge:", x.value(), y.value(), "(the concurrent add survives)")

counter after merge, both orders: 7 7
OR-set after merge: ['q3', 'urgent'] ['q3', 'urgent'] (the concurrent add survives)

CRDTs are used in production in Riak and Redis Enterprise's active-active databases, in Azure Cosmos DB's multi-region writes, in collaborative editors (Automerge and Yjs implement sequence CRDTs for text), and in local-first software that syncs devices. Their limitation is that they can only express operations whose merge is natural. A counter that must never go below zero, such as Ledgerline's account balance with an overdraft limit, cannot be a CRDT: two replicas could each approve a withdrawal that is fine alone but overdraws the account together. Such invariants require coordination, which is the deeper lesson of the CALM theorem (Hellerstein and Alvaro, 2020): programs whose outputs only grow as they learn more, called monotonic programs, can run without coordination; programs that must conclude something from the absence of information, such as "no one else withdrew", cannot.

Testing consistency claims

Data stores do not always provide the consistency they advertise. Since 2013, Kyle Kingsbury's Jepsen project has tested dozens of databases and coordination services by running concurrent operations while injecting partitions, clock skew and crashes, then checking the recorded histories against the claimed model. Many systems have been found to lose acknowledged writes or return stale reads under conditions their documentation said were safe, and most have since been fixed. The practical lessons are to read precise statements of guarantees, to understand which configuration provides them, and, for critical data, to test under failure.

Worked examples