Consistency, from one copy to many

Start where there is no problem

A single register on a single machine. Operations arrive, the machine applies them one at a time, and that is the end of it:

let x = 0
const write = (v) => { x = v }
const read  = () => x

There is no consistency question here, and it is worth being precise about why: every operation meets the same bytes. That gives you a single total order for free, and every reader necessarily sees that order, because there is nothing else to see. Anomalies are not prevented — they are unrepresentable.

So the whole subject only begins when you make a second copy. Which you will, for exactly three reasons, and it is worth knowing which one is driving you because they buy different things:

• Survival. One machine dies and takes your data with it. Copies are the only defence.
• Latency. This one is physics, not engineering. Light in fibre travels about 200,000 km/s. London to Sydney is roughly 17,000 km, so 85 ms one way and about 170 ms for a round trip — and that is the floor, before routing, queuing or processing. If a Sydney reader must reach London to read, no protocol will get them under it. A local copy is the only way out.
• Throughput. One machine has a ceiling. Copies raise the read ceiling immediately, and the write ceiling only if you shard, which is a different problem that interacts badly with this one.

And there is the cost. Copies do not merely risk staleness; they destroy the single order that made the one-copy version obviously correct. A write lands on A. A read is served by B. There is now no fact of the matter about what happened first unless something establishes one — and establishing one costs at least a round trip to whoever else has a say.

The one idea: a model is a set of admissible orders

Here is the sentence the rest of this post is deduction from.

A history is what an outside observer records: a set of operations, each with the instant it was called and the instant it returned. A consistency model is a rule saying which histories are legal. Strong models admit few histories and cost coordination. Weak models admit many and cost you the ability to reason.

That reframing does real work immediately, because it tells you what an operationis from outside: not an instant but an interval. You called it at one time; you heard back at another. What happened in between is unknowable. Two operations whose intervals overlap are concurrent, and concurrency is where all the freedom — and all the confusion — lives.

Two readers got different answers at almost the same moment — surely that is a bug? No, and this is the single most common misreading in the subject. Linearizability does not say concurrent readers agree. It says there exists some placement of each operation at an instant inside its own interval such that the whole history obeys a single-copy register. When intervals overlap, the placement has freedom, and disagreement is the visible result of that freedom. What is forbidden is disagreement that no placement can explain.

So the definition, in full: a history is linearizable if each operation can be assigned a single instant between its call and its return such that the resulting sequential order is legal for the object. Herlihy and Wing (1990). Every other model on the single-object axis is this definition with something removed.

Judging a history, by hand

The definition is not merely precise, it is decidable. Given a history you can work out on paper whether a legal order exists, and the procedure is short enough to carry in your head — which is what stops arguments about examples.

Lay the operations out as intervals, then repeatedly ask: which operation could come next? Two rules answer it.

• Real time decides what it can. An operation may go next only if no other operation still waiting finished before this one started. If something finished while this one had not yet begun, that something has already been ordered first by the world, and you have no choice about it.
• The object decides the rest. A write may always go next, and changes the value standing. A read may go next only if the value it returned is the value currently standing.

Pick any candidate satisfying both, commit to it, and repeat with what remains. Run out of candidates before you run out of operations and you back up and try a different choice. Exhaust every branch and find nothing, and you have proved no legal order exists — the history is not linearizable. That is the entire algorithm, due to Wing and Gong.

Run it on the stale read two figures above and it ends almost immediately. The write finished before the read started, so by the first rule the write must be placed first. The value standing is now 1. The only remaining operation is a read that returned 0, and the second rule forbids it. There are no other branches to try. No legal order — and notice that we established that without knowing anything whatsoever about the database that produced it.

Now the part worth pausing on. Delete the first rule — keep the object’s rules, and keep the requirement that each process’s own operations appear in the order it issued them — and the identical procedure decides sequential consistency instead. The models on this axis are not a list to be memorised. They are one procedure with a constraint added or taken away, which is why the next section can derive the rest of them by subtraction.

// A linearizability checker for a single register.
//
// Pure and total (code_guidelines.md §2): it takes a history and returns either
// an order that explains it or null. No clock, no randomness, no I/O — the
// "time" in a history is data the caller supplies, which is the only way a
// property about time can be tested deterministically.
//
// The algorithm is Wing & Gong's: try to build a linearization one operation at
// a time, backtracking when the choice turns out to be impossible.

/** An operation as an outside observer sees it: it *started* at some instant
 *  and *finished* at a later one, and took effect at some unknowable point in
 *  between. Concurrency is exactly the case where two intervals overlap. */
export type Op = {
  readonly proc: string
  readonly kind: 'write' | 'read'
  readonly value: number
  readonly start: number
  readonly end: number
}

/** The two rules of a sequential register, which is the specification every
 *  linearization is checked against. Everything else in this file is search. */
function step(state: number, op: Op): number | null {
  if (op.kind === 'write') return op.value
  return op.value === state ? state : null // a read must return what is there
}

function search(pending: readonly Op[], state: number, acc: readonly Op[]): readonly Op[] | null {
  if (pending.length === 0) return acc

  // An operation may go next only if no other pending operation *finished*
  // before it *started* — that one line is the whole of the real-time
  // constraint, and dropping it is what turns this into a check for sequential
  // consistency instead.
  const earliestEnd = Math.min(...pending.map((o) => o.end))

  for (const op of pending) {
    if (op.start > earliestEnd) continue
    const next = step(state, op)
    if (next === null) continue
    const found = search(pending.filter((o) => o !== op), next, [...acc, op])
    if (found !== null) return found
  }
  return null
}

/** The linearization, if one exists. `null` means no ordering of these
 *  operations both respects real time and obeys the register's specification —
 *  which is precisely what "this history is not linearizable" means. */
export function linearize(history: readonly Op[], initial = 0): readonly Op[] | null {
  return search([...history], initial, [])
}

export const isLinearizable = (history: readonly Op[], initial = 0): boolean =>
  linearize(history, initial) !== null

/** Sequential consistency keeps per-process order but drops the cross-process
 *  real-time constraint, so it is the same search with the one line removed. */
export function isSequentiallyConsistent(history: readonly Op[], initial = 0): boolean {
  const seqSearch = (pending: readonly Op[], state: number, taken: Map<string, number>): boolean => {
    if (pending.length === 0) return true
    for (const op of pending) {
      // Each process's own operations must still be consumed in their issue
      // order; nothing else constrains the interleaving.
      const mine = history.filter((o) => o.proc === op.proc)
      if (mine[taken.get(op.proc) ?? 0] !== op) continue
      const next = step(state, op)
      if (next === null) continue
      const advanced = new Map(taken).set(op.proc, (taken.get(op.proc) ?? 0) + 1)
      if (seqSearch(pending.filter((o) => o !== op), next, advanced)) return true
    }
    return false
  }
  return seqSearch([...history], initial, new Map())
}

Where the intuition actually fails: R + W > N

Now let us point the checker at the piece of folklore that most deserves it. Everyone learns the quorum rule: with N replicas, if read quorum plus write quorum exceeds N, every read set overlaps every write set, so reads see the latest write. N=3, R=2, W=2. Strong consistency, allegedly.

It is not, and the counterexample is embarrassingly ordinary — no partition, no crash, no clock skew, nothing exotic at all.

Three replicas, A, B and C, all holding 0. A writer begins writing 1. Writes do not arrive everywhere at once, so picture the instant at which it has reached A and not yet B. That is not a failure; it is simply the middle of a perfectly healthy write.

Reader one asks A and C. That is two replicas, so its quorum is satisfied. A holds version 1, C holds version 0, the higher version wins, and the read returns 1.

Reader two starts after reader one has already returned, and asks B and C. Both still hold version 0. It returns 0.

One read saw the new value. A strictly later read — one that had not even been issued when the first returned — saw the old one. Time went backwards for an outside observer, and by the first rule of the previous section there is no order that explains it: the read returning 1 must follow the write, and the read returning 0 must both follow that read and precede the write.

Rather than leave that as an argument, the post runs it. A simulated three-replica cluster performs exactly that schedule, the resulting history is handed to the checker from the previous section, and the verdict below is whatever the checker returned when this page was built:

The first row is not linearizable. It is, however, sequentially consistent — and that is the more useful half of the result. Dropping read repair does not hand you a broken system. It hands you a weaker model, one that is perfectly self-consistent and that nobody wrote down in the design document.

// A replicated register, simulated, so that the histories the checker judges
// are produced by a mechanism rather than written by hand.
//
// Pure (code_guidelines.md §2): the cluster is a value passed in and returned,
// there is no clock — "time" is a counter the scenario advances — and no
// randomness, so every history below is reproducible byte for byte.

import type { Op } from './checker.ts'

/** One replica holds a value and the version that stamped it. Versions are what
 *  let a reader pick a winner among disagreeing replicas. */
export type Replica = { value: number; version: number }
export type Cluster = Replica[]

export const cluster = (n: number): Cluster =>
  Array.from({ length: n }, () => ({ value: 0, version: 0 }))

/** Send a value to a chosen set of replicas. A *partial* write — one that
 *  reached fewer than W — is not an error case bolted on afterwards; it is what
 *  every in-flight write looks like, and the reason quorum overlap alone is not
 *  enough. */
export function writeTo(c: Cluster, targets: readonly number[], value: number, version: number): void {
  for (const i of targets) {
    const r = c[i]
    if (r !== undefined && version > r.version) { r.value = value; r.version = version }
  }
}

/** Read from a set of replicas and take the highest version seen.
 *
 *  `repair` is the entire difference between a quorum read and the ABD
 *  algorithm: write the winning value back to the replicas you read from before
 *  returning it, so the value you just showed someone cannot subsequently
 *  un-happen. */
export function readFrom(c: Cluster, targets: readonly number[], repair: boolean): number {
  let best: Replica = { value: 0, version: -1 }
  for (const i of targets) {
    const r = c[i]
    if (r !== undefined && r.version > best.version) best = r
  }
  if (repair && best.version >= 0) writeTo(c, targets, best.value, best.version)
  return best.value
}

export type Scenario = { readonly label: string; readonly history: readonly Op[] }

/** The canonical quorum failure, N=3 W=2 R=2.
 *
 *  A writer is mid-flight: its value has reached one replica. Two reads follow,
 *  the second starting strictly after the first finished, and they disagree —
 *  the later one goes backwards. Set `repair` to run ABD instead and watch the
 *  same schedule become linearizable.
 */
export function partialWrite(repair: boolean): Scenario {
  const c = cluster(3)
  const history: Op[] = []

  // The write is in progress throughout: it has reached replica 0 and not yet
  // replica 1, so its interval spans both reads.
  writeTo(c, [0], 1, 1)
  history.push({ proc: 'writer', kind: 'write', value: 1, start: 0, end: 60 })

  const first = readFrom(c, [0, 2], repair)
  history.push({ proc: 'reader-a', kind: 'read', value: first, start: 10, end: 20 })

  const second = readFrom(c, [1, 2], repair)
  history.push({ proc: 'reader-b', kind: 'read', value: second, start: 30, end: 40 })

  return { label: repair ? 'quorum + read repair (ABD)' : 'quorum read, R+W>N', history }
}

/** A read served by a replica that has not caught up. The write completed
 *  before the read began, so no ordering can explain the stale answer. */
export function staleRead(): Scenario {
  return {
    label: 'async replica, stale read',
    history: [
      { proc: 'writer', kind: 'write', value: 1, start: 0, end: 10 },
      { proc: 'reader', kind: 'read', value: 0, start: 20, end: 30 },
    ],
  }
}

/** Concurrency is not an anomaly. Both reads overlap the write, so a linearizer
 *  is free to place the write between them. */
export function concurrentOk(): Scenario {
  return {
    label: 'overlapping write, disagreeing reads',
    history: [
      { proc: 'writer', kind: 'write', value: 1, start: 0, end: 40 },
      { proc: 'reader-a', kind: 'read', value: 0, start: 5, end: 15 },
      { proc: 'reader-b', kind: 'read', value: 1, start: 20, end: 35 },
    ],
  }
}

/** Each process sees a self-consistent order, but no single order explains
 *  both — the classic separation between sequential consistency (which this
 *  passes) and linearizability (which it fails). */
export function sequentialNotLinearizable(): Scenario {
  return {
    label: 'each process consistent, no global order in real time',
    history: [
      { proc: 'a', kind: 'write', value: 1, start: 0, end: 10 },
      { proc: 'b', kind: 'write', value: 2, start: 20, end: 30 },
      { proc: 'a', kind: 'read', value: 1, start: 40, end: 50 },
    ],
  }
}

So the quorum rule is wrong? No — it is precisely right about a smaller thing than people remember. It guarantees that a read set intersects the write set of every completed write. The counterexample uses a write that has not completed, and for that one the rule promises nothing at all. The error is not in the arithmetic; it is in dropping the word “completed” when repeating it.

The fix is one line, and it is the ABD algorithm (Attiya, Bar-Noy and Dolev, 1995): a read writes back the value it is about to return, before returning it. Then a value that has been shown to anyone is already durable enough that the next read cannot miss it — which is exactly what the second row above shows. The cost is that reads now perform writes, so a read-heavy workload pays write amplification for a property most of those reads did not need. That is the trade, stated honestly, and it is why Dynamo-style stores that skip it are not lying; they are selling something else.

The models, derived rather than listed

Take linearizability and remove one constraint at a time. Each removal has a name, and each admits strictly more histories.

• Drop real time across processes, keep a single order. That is sequential consistency (Lamport, 1979). Everyone agrees on one order and each process’s own operations appear in the order it issued them — but that order need not match the wall clock. A write that finished an hour ago may be ordered after a read that happened now.
• Drop the single order; keep it only for causally related operations. Causal consistency. If I read your post and then reply, nobody sees my reply before your post. Two unrelated posts may be seen in either order by different readers. This is the strongest model that stays available under partition (Mahajan et al., 2011) — which makes it far more interesting than its popularity suggests.
• Drop cross-client promises; keep promises to one client. The session guarantees (Terry et al., 1994): read-your-writes, monotonic reads, monotonic writes, writes-follow-reads. Cheap, and they remove most of what users actually notice.
• Drop everything except convergence. Eventual consistency: if writes stop, replicas agree. Note what it does not say — no bound on when, and no promise whatsoever before then. “Eventually” is not a latency figure.

If sequential consistency gives everyone one agreed order, why would anyone pay for linearizability? Because of the channel your system cannot see. Two users on a phone call, one clicking “pay” and telling the other to refresh; a service writing to a database and then posting to a queue that another service reads. Sequential consistency permits the second observer to see the world before the write, and the out-of-band message is what makes that visible as a bug. Linearizability is exactly the model that composes with the real world, because real time is the one channel everything shares. It is also why linearizability is local — compose linearizable objects and the result is linearizable — which is not true of sequential consistency.

The other axis, which is not the same axis

Everything above concerns one object. Transactions concern several, and the vocabulary collides badly: the C in ACID means “your invariants hold”, which is your job and not the database’s. The word that matters for transactions is isolation.

Serializability says the outcome equals some serial execution of the transactions. Note what it does not say: which one, or that it has anything to do with real time. A serializable database may legally order a transaction that committed an hour ago after one running now. Strict serializability is serializability plus linearizability — one serial order, and it respects real time. Spanner calls it external consistency.

The weaker isolation levels are best understood by what they let through, not by their names — the names are historically confused. ANSI SQL defined levels by which anomalies they forbid, Berenson et al. (1995) showed the definitions were ambiguous and did not capture snapshot isolation at all, and Adya (1999) gave the definitions people actually use now. The practical residue: PostgreSQL’s REPEATABLE READ is snapshot isolation, Oracle’s SERIALIZABLE is snapshot isolation too, and only one anomaly separates SI from the real thing.

invariant: at least one doctor on call
T1  read(on_call) → {alice, bob}
T2  read(on_call) → {alice, bob}
T1  alice off call; COMMIT
T2  bob off call;   COMMIT    ← nobody on call

The transaction axis is a subject of its own, and it has its own post — Transactions, when everyone writes at once — which derives the anomalies from conflict cycles and walks through locking, MVCC and SSI. Everything you need for this post is here; that one is a neighbour, not a missing half.

That last anomaly, write skew, deserves its reputation. Each transaction reads a set of rows, checks an invariant, and writes a different row. Each is individually correct. Under snapshot isolation neither sees the other’s write, because first-committer-wins only catches transactions writing the same row. Together they break the invariant. The on-call roster, the meeting-room booking, the account that must not go negative across two balances — all the same shape.

Why not just always use serializable? Often you should; the default reason not to is worse than people think it is. The honest cost is not that serializable is uniformly slower — modern SSI (Cahill et al., 2008, shipped in PostgreSQL since 9.1) is competitive at low contention. The cost is that it fails by aborting. At high contention, throughput does not gracefully degrade; it collapses, as a rising share of transactions abort and retry, adding load. Every caller needs retry logic that is actually correct. That is the real bill, and it is paid in operational complexity rather than in milliseconds.

CAP, stated properly, and the part that matters more

The theorem (Gilbert and Lynch, 2002, formalising Brewer’s conjecture): in an asynchronous network in which messages may be lost, no implementation can be both available and atomic — where atomic means linearizable. That is it.

Three corrections, all load-bearing:

• You do not pick two of three. Partitions are not a design choice; the network does what it does. The choice is what you do during one, so the theorem offers two options, not three.
• The C is linearizability, not the C in ACID. They are unrelated properties that happen to share a letter.
• Partitions are rare; the tax is daily. This is the important one.

Abadi’s PACELC (2012) is the formulation worth carrying: if Partitioned, choose Availability or Consistency; Else — which is almost always — choose Latency or Consistency. The second clause is the one you pay for on a normal Tuesday, and it is just the round-trip floor from the first section wearing a suit. A linearizable write must be acknowledged by a quorum; a quorum is somewhere else; somewhere else is at least one round trip away.

How it is actually built, and where each one breaks

Start with the naive approach, because it is what everyone builds first and its failure is where the rest comes from.

Is there a way to know whether I need coordination at all, rather than guessing? Yes, and it is the most underused result in the area. Bailis et al. (2014) define invariant confluence: an invariant and a set of operations are I-confluent if merging any two states that each satisfy the invariant yields a state that also satisfies it. If your workload is I-confluent, coordination is provably unnecessary — you can run it coordination-free and stay correct. If it is not, no implementation trick avoids coordination. It converts “how strong should this be?” from taste into a property you can check. Unique-username assignment is not I-confluent. Appending to a set is.

Clocks, and why the one on the wall is not one

Ordering events across machines means agreeing on time, and physical clocks disagree. NTP leaves milliseconds of skew on a good day, clocks step backwards, and virtual machines pause. Last-write-wins over wall-clock timestamps therefore does not resolve conflicts — it silently discards whichever write ran on the machine whose clock was behind.

• Lamport clocks (1978): a counter per node, advanced on send and receive. Guarantees that if A causally precedes B then C(A) < C(B). The converse does not hold, so you cannot tell concurrency from ordering.
• Vector clocks: one counter per node. Now you can detect concurrency exactly — at the cost of metadata proportional to the number of writers, which is why Dynamo-style systems struggle with them at scale.
• Hybrid logical clocks (Kulkarni et al., 2014): physical time that is never allowed to go backwards, nudged forward by causality. Close enough to wall clock to be human-readable, strong enough to respect causality. Used by CockroachDB and MongoDB.
• TrueTime (Spanner, 2012): the interesting move is admitting the uncertainty rather than hiding it. The API returns an interval guaranteed to contain the true time, with bounded error ε, backed by GPS and atomic clocks. Spanner then simply waits out 2ε before acknowledging a commit, so that commit order provably matches real time. It buys strict serializability with a hardware budget and a few milliseconds of deliberate delay.

Waiting on purpose seems like an admission of defeat — why is that a good design? Because uncertainty does not disappear if you refuse to measure it. Every other system has the same clock error; it simply does not know the bound, so it cannot wait it out and must instead avoid depending on physical time. Spanner pays a known, bounded cost in exchange for a guarantee nobody else could offer at the time. The lesson generalises: a bound you can name is worth far more than an error you have merely stopped thinking about.

Choosing, without cargo-culting

Four questions, in order. They resolve most real cases without any appeal to taste.

And one rule that saves more incidents than any of them: if the answer is “weak is fine”, add the session guarantees anyway. Read-your-writes and monotonic reads are cheap — usually a sticky routing decision or a token carried by the client — and they remove the overwhelming majority of staleness that users actually notice, which is their own writes disappearing and pages that go backwards when refreshed.

Who gives what

The table in the one-pager below lists defaults and strongest available settings per system. Two things about it matter more than its contents.

First, defaults are weak almost everywhere, and the name on the tin is often not the property in the tin: REPEATABLE READ means snapshot isolation in PostgreSQL, SERIALIZABLE means snapshot isolation in Oracle, and ZooKeeper — famously — gives linearizable writes but only sequentially consistent reads unless you call sync() first. Reading your own database’s isolation documentation is not a beginner activity.

Second, and more important: the documented guarantee and the delivered guarantee are different claims. That gap is not hypothetical, and it is the entire reason Kyle Kingsbury’s Jepsen exists — a long series of reports in which real databases, under real partitions, violated the models they advertised. The methodology is the lesson: do not reason about the implementation, record its history and check it, which is exactly what the sixty lines above do in miniature.

Where this is, as of September 2026

Dated deliberately, because this area moves and a post that reads as timeless about it is lying.

• Bounded-uncertainty clocks are becoming ordinary. TrueTime was exotic in 2012 because it needed GPS receivers and atomic clocks in every datacentre. Cloud providers now sell tightly-bounded time as a service — AWS Time Sync offers microsecond- level accuracy, and Aurora DSQL builds strongly-consistent multi-region commits on it without classical two-phase commit. The consequence is that Spanner’s design is drifting from “what Google can afford” toward “what you can rent”.
• Leaderless transaction protocols are shipping. Cassandra’s Accord (CEP-15) targets general-purpose transactions without a designated leader and with one round trip in the common case, building on the EPaxos line of work. The prize is removing the leader as both a latency floor for distant clients and a throughput ceiling.
• Verification has caught up with implementation. Elle (Kingsbury and Alvaro, 2020) infers transactional anomalies from observed histories rather than searching for serial orders, which made checking practical at sizes that defeated earlier tools. Model checking designs in TLA+ or P before building them is now normal at several large shops rather than a research curiosity.
• Local-first is the interesting frontier. Mature CRDT libraries (Automerge, Yjs) made coordination-free collaborative editing routine. The open problem is unchanged and is the one from the mechanisms table: invariants spanning objects. What is contested is how much of an application can be expressed I-confluently, and reasonable people disagree.

◆ The first and second items describe products and protocols that were moving quickly at the time of writing; treat version-specific details as things to verify, not as settled fact. The papers cited throughout are stable; the shipping status of anything is not.

The whole thing, on one page

For the second reading, and for the afternoon six months from now when you need the table rather than the argument. It prints.

Check yourself

Quick reference

Every abbreviation this post used, expanded, plus the neighbouring terms you will meet in the papers below. Ordered for lookup, not for reading.