A register x runs 0 → 1 → 2 → 4 by compare-and-set. Every read returns a value that was genuinely written, and no single operation contradicts another — yet a brute-force linearizability checker reports NOT linearizable, because client A already read the new value 4 before client B's read began, so B may not return the older 2. Flip that one read to 4 and it passes; DDIA's Figure 10-6 quorum read fails for the same reason.
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.
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.
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.
check_linearizable demands at once: real-time order and a legal register trace.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.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.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.
cd study/ddia/ch10/code
python3 linearizability_checker.pyDo 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.
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]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.
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?
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.
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]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).
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.
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.Sources: DDIA 2e, Ch. 10, §"What Makes a System Linearizable?" (Figures 10-4 and 10-6) · Herlihy & Wing, "Linearizability: A Correctness Condition for Concurrent Objects" (1990) · Gibbons & Korach, "Testing Shared Memories" (1997).