# DDIA Ch. 10: a linearizability checker rejects a history that "looks consistent"
## Concept
A register `x` starts at 0. You record a **history** of operations on it — each
op is `(process, kind ∈ {write, read, cas}, args, returned value, start_time,
end_time)`. Then you build a brute-force **linearizability checker**: it searches
for *some* sequential (total) order of the ops that (a) respects real time — if
op X finishes before op Y starts, X must come before Y — and (b) is a legal
register trace — each read returns the current value, and `cas(old, new)`
succeeds only when the current value is `old`. Feed it DDIA's Figure 10-4
history, where every read returns a value that was genuinely written and no
single operation contradicts another. A careful reader declares it consistent.
The checker reports **NOT linearizable** — because client A already read the new
value 4 before client B's read *began*, so B is forbidden from returning the
older 2. The aha: "no read returned an invented value ⇒ consistent" is wrong. The
violation is a cross-client **recency** constraint that is invisible op by op.
## Provenance
*Designing Data-Intensive Applications*, 2nd ed. (Kleppmann & Riccomini, 2025),
Chapter 10 — *Consistency and Consensus*, §"What Makes a System Linearizable?"
(Figure 10-4):
> the final read by B is not linearizable [...] B is not allowed to read an older
> value than A.
The book draws linearizability as the illusion of a single, up-to-date copy of
the data: as soon as one read returns the new value, every later read must too.
Figure 10-6 then shows a Dynamo-style quorum (`w + r > n`) that *still* returns a
stale value, so it is not linearizable either. This exercise turns both figures
into recorded histories and lets the checker deliver the verdict.
## Prerequisites
The result rides on one idea — a real-time recency edge *between* operations —
so that line is flagged. Each note says where the concept shows up.
1. **Linearizability = a single, up-to-date copy + real-time recency** — the
register must behave as if there were one copy and every op took effect
atomically at one instant between its start and end. It shows up as the two
things `check_linearizable` demands at once: real-time order *and* a legal
register trace.
2. **A history and its partial order** — overlapping ops are unordered (either
may take effect first); only non-overlapping ops (`X.end < Y.start`) get a
real-time edge. It shows up as `must_before[i][j]`, the constraint the search
may never violate. **← this recency edge carries the whole result.**
3. **Register semantics (read / write / compare-and-set)** — a read returns the
last write; `cas(old,new)` mutates only if the current value is `old`. It
shows up as the replay loop that rejects an order the moment a read or cas is
illegal.
4. **Linearizability ≠ serializability** — serializability is about transactions
appearing to run in *some* serial order (isolation); linearizability is about
*single-object* reads/writes appearing in *real-time* order (recency). A store
can be one without the other. It shows up as the fact that Figure 10-4 has no
transactions at all, yet still fails.
### Where to learn the prerequisites
- **Linearizability, histories, the recency constraint (#1–#3):** DDIA
§"What Makes a System Linearizable?"; Herlihy & Wing, "Linearizability: A
Correctness Condition for Concurrent Objects" (1990) for the original
definition and the history/partial-order machinery.
- **Linearizability vs serializability (#4):** DDIA §"Linearizability versus
serializability"; Peter Bailis, "Linearizability versus Serializability"
(bailis.org/blog) — a free, one-page disentangling of the two.
If only one is new, make it **#2** — the real-time edge between B's read and A's
read is the entire reason Figure 10-4 fails, and it is exactly what an op-by-op
"did this read return a written value?" check cannot see.
## Environment
macOS 26.5.2 (Darwin 25.5.0), arm64; Python 3.15.0a8, standard library only; no
Docker; histories are fixed inputs and the checker is deterministic, so verdicts
reproduce exactly.
## Mental model
Linearizability is a geometry claim: for each operation there exists a single
**instant** — somewhere between when it started and when it finished — at which
it "takes effect," and if you collapse every op onto its instant, the resulting
left-to-right sequence is a legal register trace. The checker looks for exactly
those instants. It can slide any op's instant anywhere inside its own time bar
(that is the freedom overlapping ops get), but it can never move an op's instant
outside its bar — so if op X's bar ends before op Y's bar begins, X's instant is
unavoidably to the left of Y's.
Concretely, `check_linearizable` enumerates every total order of the ops, throws
away the ones that put some op before another it must follow in real time, and
replays each survivor against a plain register (read returns current value; cas
checks `old`). If any survivor replays cleanly, that order *is* the set of
instants — the history is linearizable and the order is a witness. If none do,
no such instants exist and the history is rejected. It is a search, so it is
exponential; that is fine for these tiny histories and is the point of the
boundary note at the end.
## Setup
```
cd study/ddia/ch10/code
python3 linearizability_checker.py
```
Do **not** read the output yet — make each prediction first. The whole script is
`code/linearizability_checker.py`; the histories are fixed and deterministic, so
your run matches the transcripts below exactly.
## Steps
### Step 1 — Figure 10-4: consistent-looking, but is it linearizable?
**Predict.** Here is the recorded history. `x` starts at 0 and climbs 0 → 1 → 2 →
4 via compare-and-set. Client A reads 1, then 2, then 4; then client B's read
*starts* at t=18 (after A's read of 4 finished at t=17) and returns 2. Every read
returns a value that was really written, and no single op contradicts another.
Will the checker call it linearizable?
```
C: cas(0, 1) = ok [t 1..4 ]
A: read() = 1 [t 5..7 ]
B: cas(1, 2) = ok [t 6..9 ]
A: read() = 2 [t 10..12]
D: cas(2, 4) = ok [t 11..14]
D: cas(2, 3) = fail [t 13..16]
A: read() = 4 [t 15..17]
B: read() = 2 [t 18..20]
```
**Observe.**
```
============================================================
History 1 -- DDIA Figure 10-4 (x: 0 -> 1 -> 2 -> 4 via cas)
============================================================
C: cas(0, 1) = ok [t 1..4 ]
A: read() = 1 [t 5..7 ]
B: cas(1, 2) = ok [t 6..9 ]
A: read() = 2 [t 10..12]
D: cas(2, 4) = ok [t 11..14]
D: cas(2, 3) = fail [t 13..16]
A: read() = 4 [t 15..17]
B: read() = 2 [t 18..20]
Every read returned a value that was genuinely written (0,1,2,4 all appear),
and no single operation contradicts another on its own.
VERDICT: NOT linearizable.
Reason (real-time recency): A's read returned 4 (version rank 3) and finished at t=17;
B's read began later at t=18 but returned 2 (version rank 2).
Once a completed read has observed the newer value, no later read may
return an older one -- and no write reverts it back. No sequential
order can respect both real time and the register semantics.
```
**NOT linearizable.** The `cas(2,3)` even fails cleanly (the value is already 4),
and every read is of a genuinely-written value. The single thing wrong is a
*relationship between two reads*: A finished reading 4 before B started, so in
any real-time-respecting order A's read is left of B's — and once the register is
4, nothing pushes it back to 2.
### Step 2 — the control: change one read, and it passes
**Predict.** Keep every operation identical, but let B's final read return **4**
instead of 2. One value changes. Does the checker now find a legal order — or is
it a rubber stamp that rejects everything with concurrency?
**Observe.**
```
============================================================
History 2 -- control: identical ops, but B's last read returns 4
============================================================
C: cas(0, 1) = ok [t 1..4 ]
A: read() = 1 [t 5..7 ]
B: cas(1, 2) = ok [t 6..9 ]
A: read() = 2 [t 10..12]
D: cas(2, 4) = ok [t 11..14]
D: cas(2, 3) = fail [t 13..16]
A: read() = 4 [t 15..17]
B: read() = 4 [t 18..20]
The only change from History 1 is B's final read: 4 instead of 2.
VERDICT: linearizable.
A legal, real-time-respecting order exists. Replaying it on x (start 0):
1. C: cas(0,1)=ok x: 0 -> 1
2. A: read()=1 x = 1 (matches)
3. B: cas(1,2)=ok x: 1 -> 2
4. A: read()=2 x = 2 (matches)
5. D: cas(2,4)=ok x: 2 -> 4
6. D: cas(2,3)=fail x = 4 (current 4 != 2, cas fails)
7. A: read()=4 x = 4 (matches)
8. B: read()=4 x = 4 (matches)
```
**Linearizable.** The checker prints a witness — an actual total order that
respects every real-time edge and replays cleanly, including the failing
`cas(2,3)` landing where the value is already 4. One flipped read is the entire
difference between accept and reject, which is the sharpest possible evidence
that the checker is testing the *recency relationship*, not merely whether each
read is of some written value.
### Step 3 — Figure 10-6: a quorum read with `w + r > n`, still stale
**Predict.** Now a Dynamo-style quorum. A long write of 1 (initial 0) overlaps
two reads. Client B reads the new value 1; client C, whose read *starts* after
B's finished, reads the old 0 — the stale quorum read the book warns about. Quorum
math says `w + r > n`, so the read and write quorums overlap. Does that make the
history linearizable?
```
W: write(1) = ok [t 1..12]
B: read() = 1 [t 4..6 ]
C: read() = 0 [t 8..10]
```
**Observe.**
```
============================================================
History 3 -- DDIA Figure 10-6 (quorum read, w + r > n, still stale)
============================================================
W: write(1) = ok [t 1..12]
B: read() = 1 [t 4..6 ]
C: read() = 0 [t 8..10]
A quorum write of 1 overlaps both reads. B reads the new value, C the old --
yet C's read starts after B's finished.
VERDICT: NOT linearizable.
Reason (real-time recency): B's read returned 1 (version rank 1) and finished at t=6;
C's read began later at t=8 but returned 0 (version rank 0).
Once a completed read has observed the newer value, no later read may
return an older one -- and no write reverts it back. No sequential
order can respect both real time and the register semantics.
```
**NOT linearizable.** Exactly the same shape as Figure 10-4, with the version
chain shortened to `0 → 1`: an earlier read saw the newer value, a strictly later
read saw the older one. `w + r > n` guarantees the quorums *intersect*, not that
reads see writes in real-time order — so a quorum store is not linearizable
without extra work (read repair on every read, synchronously).
## What you should see
- **History 1 (Figure 10-4):** NOT linearizable. A read 4 (finished t=17); B's
read started t=18 and returned the older 2.
- **History 2 (control):** linearizable — the checker prints an 8-step witness
order that replays cleanly.
- **History 3 (Figure 10-6):** NOT linearizable. B read 1 (finished t=6); C's
read started t=8 and returned the older 0.
- The only difference between the rejected History 1 and the accepted History 2
is one read's returned value.
## Why
Op by op, Figure 10-4 is spotless: `cas(0,1)`, `cas(1,2)`, `cas(2,4)` each fire
on the right current value; `cas(2,3)` fails honestly; and every read returns 0,
1, 2, or 4 — all values that were really written. A checker that asked only "did
this read return a value that exists in the write history?" would pass it. That
question is *local* to each operation, and linearizability is not a local
property.
Linearizability is a claim about a single **global real-time order**. Each op
takes effect at one instant inside its own time bar, and the collapsed sequence
of instants must be a legal register trace. The load-bearing consequence: if op X
finishes before op Y starts, X's instant is necessarily to the left of Y's —
there is no interval left for them to swap. In Figure 10-4, A's `read()=4`
finishes at t=17 and B's `read()=2` starts at t=18. No overlap, so A's instant is
left of B's, full stop. But the register reaches 4 only *after* `cas(2,4)`, and
nothing ever moves it back to 2. So at B's instant — which is after A's, which is
after the register became 4 — the current value is 4, and B cannot legally return
2. Every candidate order the search tries dies on this one edge. That edge exists
*between* two reads by *different* clients; it is precisely the recency
constraint an op-by-op check cannot represent, because it is not a fact about any
single operation. Figure 10-6 is the same failure with a two-value chain: the
quorum overlap `w + r > n` buys intersection, not real-time recency, so B's fresh
read followed by C's stale read forms the identical newer-then-older edge.
The witness in History 2 shows the flip side. With B reading 4, the search finds
an order — `cas(0,1)`, `read 1`, `cas(1,2)`, `read 2`, `cas(2,4)`, the failing
`cas(2,3)` (landing where the value is already 4), `read 4`, `read 4` — that
honors every real-time edge and replays legally. A single value change is the
whole difference, because the recency edge only bites when the later read
disagrees.
**The boundary — the constraint only bites when operations overlap.** Take any
history with no concurrency — every op's bar ends before the next one's begins —
and the real-time partial order becomes a *total* order. There is exactly one
candidate for the search, and it is linearizable iff it replays legally, i.e.
iff it is a valid single-threaded register trace. All the subtlety vanishes:
recency and "reads a written value" coincide when nothing overlaps. Linearizability
is *only* interesting under concurrency; it is the extra promise that concurrent,
overlapping operations still line up as if they had run one at a time in real-time
order.
### Go deeper
1. **Watch the search cost explode.** The checker is `O(n!)` in the worst case —
deciding linearizability of a general history is NP-hard (Gibbons & Korach,
1997). Add a few more overlapping ops and time it; this is why real tools
(Jepsen's **Knossos**, and its faster successor **Elle**) use smarter
pruning and still bound history length.
2. **Make Figure 10-6 pass.** Add a synchronous read-repair: model C's read as
also writing back the newest value it saw, or shrink the write's time bar so
it finishes before C starts. Re-run and watch the verdict flip to
linearizable — the fix DDIA names for making quorums linearizable.
3. **Serializable but not linearizable.** Build a history of two *transactions*
that is serializable (some serial order exists) yet violates real-time order,
and confirm this register checker is the wrong tool for it — sharpening why
the two guarantees are independent.