A concurrent object gives you a pleasant lie:

operations overlap in time
but the object behaves
as if each operation happened
at one instant

Linearizability is the discipline of making that lie precise.

The point is not that operations literally take effect at visible timestamps. The point is that the history must admit a legal fiction. For every completed operation, you should be able to choose one instant between its invocation and its response. If you sort operations by those chosen instants, the resulting sequential story must obey the object’s ordinary specification.

For a register, that specification is boring:

write(v) sets the value to v
read() returns the current value
cas(expected, update)
  succeeds iff current == expected

The boringness is the feature. Linearizability lets you reason about concurrent objects using their sequential meanings, while still permitting real overlap. Herlihy and Wing’s original paper framed the condition exactly this way: each operation appears to take effect instantaneously somewhere between call and return, and non-overlapping operations must keep their real-time order.1

That “somewhere” does a lot of work.

The Window Is Evidence

Consider this register history, initially 0:

time: 1  2  3  4  5  6  7  8
W1:   write(1) --------------
R0:      read() -> 0 ---
R1:               read() -> 1 ---

This history can be linearizable. Put R0 before W1, because their intervals overlap and R0 returned the old value. Put R1 after W1, because its interval also overlaps enough to let the write take effect first.

One legal sequential explanation is:

read -> 0
write 1
read -> 1

No thread observed magic. We just used the uncertainty inside the overlapping call intervals.

Now make one tiny edit:

W1: write(1) returns before R0 starts
R0: read() -> 0

The overlap is gone. Real time creates a hard edge: W1 must be before R0. The sequential register says a read after write(1) must return 1. There is no legal instant left for R0.

That is the shape of a linearizability bug. Not “a stale read feels bad,” but “no sequential explanation exists.”

A Tiny Checker

The lab below performs an exact search over small histories. It builds the real-time precedence graph, then tries every operation whose predecessors have already been placed. Each candidate is applied to a sequential register or compare-and-set model. If the return value does not match the current state, that branch dies.

This is essentially the small version of the history-search idea that appears in testing work by Wing and Gong, later explored and optimized in linearizability testing algorithms such as Lowe’s.23 Production checkers have to care about state explosion. This notebook keeps the histories tiny so the reasoning remains visible.

Try these cases:

  • Overlap can save a read: a read returning 0 is legal because it can be placed before an overlapping write.
  • Completed write ignored: a read starts after write(1) returns but still reports 0; the checker exhausts every branch.
  • Read sees future: a read finishes before the write begins yet returns the future value.
  • Two successful CAS calls: overlap cannot make two cas(0, *) calls both succeed on one register.

    The audit covers six histories, checks expected valid/invalid verdicts, verifies the overlap witness order, and confirms that the CAS-duel case dies by sequential semantics rather than by timing alone.

    The reason a checker searches rather than simply sorting by start time is that overlap creates freedom. A slow write(1) may linearize near the beginning of its call or near the end. A read overlapping it may legally return either old or new value, depending on where the chosen instants land.

    But the freedom is not unlimited. The chosen order must satisfy two constraints:

    • Real-time constraint: if operation A returns before operation B is called, then A must be before B.
    • Object constraint: the sequential return values must be legal for the data type.

    The lab’s backtracking search is tiny, but it captures that structure. For the CAS duel, both calls overlap completely, so real time does not decide the order. The object does. If cas(0,1) succeeds first, the value is no longer 0, so cas(0,2) cannot also succeed. Reversing the order has the same problem. The history is nonlinearizable even though there is plenty of overlap.

    This is why linearizability is stricter than “could be concurrent.” It demands a single sequential explanation, not just a collection of individually plausible responses.

    Distributed Systems Make the Histories Messy

    In distributed testing, the object might be a key-value register, a queue, a set, or a compare-and-set register exposed over a network. Clients record invocations and completions. A checker such as Knossos then asks whether the observed history can be explained by a sequential model.4 Jepsen uses this kind of checker for linearizable objects, while also using other checkers for weaker or transactional guarantees.5

    This matters because a single successful read can be more damning than a pile of timeouts. A timeout may leave an operation pending; maybe it happened, maybe it did not. But a completed read returning a value that cannot fit anywhere in the history is a proof-shaped failure.

    There is a second practical lesson: linearizability is local. Herlihy and Wing emphasized that a system is linearizable if each individual object is linearizable.1 That locality is why many tests split histories by key. It is also why a single-key register can be easier to verify than a multi-key transactional story. The hard part moves from “one object” to “which object did this operation really touch?”

    The Useful Lie

    Linearizability does not say the implementation is simple. It says the outside history has a simple explanation.

    That distinction is the whole trick. Inside the object there may be locks, compare-and-swap loops, replication, retries, leader changes, speculative reads, or cache effects. Outside, if the object is linearizable, clients may pretend there was one instant per operation.

    When the checker fails, it is not accusing the system of being slow. It is accusing the system of having no possible instant.

    The operation did not merely return the wrong value.

    It returned a value that had nowhere to stand.

    1. Maurice P. Herlihy and Jeannette M. Wing, “Linearizability: A Correctness Condition for Concurrent Objects”, ACM Transactions on Programming Languages and Systems, 1990. ↩ ↩2

    2. Jeannette M. Wing and Chun Gong, “Testing and Verifying Concurrent Objects”, Journal of Parallel and Distributed Computing, 1993. ↩

    3. Gavin Lowe, “Testing for Linearizability”, 2015. ↩

    4. Jepsen, “Knossos”, a checker for experimentally accessible linearizability histories. ↩

    5. Jepsen checker documentation, “linearizable”, which describes validation through Knossos. ↩