Symptom
Your key-value store returns the wrong answer, or so a user says. Thread A wrote
x = 5 and got an acknowledgement. Thread B then read x and got 4.
You check the logs. Both operations succeeded. No error, no partition, no timeout. You look for a race in the storage layer and cannot find one. Then someone asks the question that reframes it: what does “then” mean? A’s write returned at 12:00:00.003 and B’s read started at 12:00:00.007, by two clocks you do not trust, in two processes, across a network.
You need a correctness condition. “The answer is what a single-threaded program would have given” is not yet a definition, because a concurrent execution has no single-threaded program to compare against — operations overlap. Until you can say precisely which concurrent histories are acceptable, you cannot say whether this is a bug, and you certainly cannot test for it.
Statement
An execution is a history: a sequence of invocation and response events on shared objects. An operation’s interval runs from its invocation to its response, and two operations are concurrent if their intervals overlap.
Linearizability. A history is linearizable if each operation appears to take effect instantaneously at some single point — its linearization point — between its invocation and its response, and the resulting sequential history is legal for the object’s sequential specification.
Two consequences make the definition worth having.
Real-time order is respected. If operation $A$ responds before operation $B$ is invoked, then $A$ precedes $B$ in the linearization. Non-overlapping operations cannot be reordered.
Locality (composition). A history is linearizable if and only if its restriction to each object is linearizable. Linearizable objects compose; a system built from linearizable parts is linearizable for free.
The mental image: every operation is a segment on the timeline, and you must place one dot inside each segment so that reading the dots left to right gives a legal sequential execution. Concurrent operations may be ordered either way, because their segments overlap and the dots can go in either order. Non-concurrent operations may not.
Argument
Why real-time order is the load-bearing clause. Drop it and you get sequential consistency: operations appear in some total order consistent with each thread’s program order, with no constraint tying that order to real time. Sequential consistency permits a read to return a value written arbitrarily far in the past, as long as no thread observes an inconsistency, which is exactly the failure the symptom describes.
Linearizability forbids it. A wrote 5 and the write returned; B’s read started afterwards; therefore the linearization point of the write precedes that of the read; therefore the read must return 5 or a later value. Returning 4 is unambiguously a bug, and you now have a statement you can test rather than an intuition you can argue about.
Why locality is the property that actually pays. Sequential consistency is not local: two individually sequentially-consistent objects can be combined into a system that is not sequentially consistent. That is not a technicality. It means you cannot verify a system module by module.
Sketch of locality. Let $H$ be a history whose restriction $H|x$ is linearizable for every object $x$. Each $H|x$ has a witness linearization $S_x$, inducing a total order $<_x$ on that object’s operations. Define a relation on all operations by the union of the $<_x$ together with the real-time order $<_H$.
The proof shows this union is acyclic. A cycle would have to alternate between objects, since each $<_x$ is a total order and is therefore itself acyclic. Take a minimal cycle; walking around it, each step is either within an object or a real-time edge. Because every $S_x$ respects real-time order on its own object, any such cycle forces an operation to precede itself in real time, which is impossible for intervals on a line. Acyclic means it has a topological extension, and that extension is a linearization of $H$.
The consequence is the one worth carrying: the reason you can use a linearizable queue and a linearizable map together without re-verifying their interaction is a theorem, not luck.
Where the linearization point actually sits. For a lock-based object it is easy: any point inside the critical section, conventionally the moment the state changes. For lock-free code it is subtler and is the standard proof obligation. In the Michael–Scott queue, an enqueue linearizes at the successful CAS that links the new node, even though the operation continues afterwards to swing the tail pointer. A dequeue on an empty queue linearizes at the read that observed emptiness.
The interesting case is that an operation’s linearization point may depend on other threads’ behaviour, and may even lie in code executed by a different thread that helped complete it. That is why linearizability proofs are done against histories rather than against code.
Distinguishing the three conditions people conflate.
| Condition | Total order? | Respects real time? | Local? | Typical home |
|---|---|---|---|---|
| Linearizability | yes, one order | yes | yes | single objects, registers, etcd |
| Sequential consistency | yes, one order | no | no | memory models (T056) |
| Serializability | yes, over transactions | no | no | databases (T071) |
| Strict serializability | yes, over transactions | yes | yes | Spanner, FoundationDB |
Serializability and linearizability are frequently treated as the same idea at different scales, and the difference matters twice. Serializability is about multi-operation transactions and says the interleaving is equivalent to some serial order — possibly one that puts a transaction committed an hour ago after one committed just now. Linearizability is about single operations on a single object and pins the order to real time. Neither implies the other. Their conjunction is strict serializability, which is what “externally consistent” systems advertise.
The cost, stated honestly. Linearizability requires that a read see the result of every completed write, which in a replicated system means a read cannot be served from a stale replica without coordination. Under a network partition this is precisely the CAP tension (T066): linearizability is the C, and a partitioned system must sacrifice it or sacrifice availability. Quorum intersection (T065) is the usual construction, and $R + W > N$ with a read-repair or a leader lease is how most systems buy it.
Testing for it, which is unusually tractable. Checking whether an arbitrary history is linearizable is NP-complete in general, since it amounts to searching orderings of concurrent operations. In practice it is very checkable: Jepsen’s Knossos and Elle checkers take recorded histories from a real cluster under fault injection and search for a valid linearization, and they have found real violations in Etcd, MongoDB, Redis, and many others. This is one of the rare correctness conditions with an industrial-grade automated checker, which is a large part of why it became the standard.
Forbids
A read that returns a value older than a completed write. If the write responded before the read was invoked, real-time order forces the linearization, and any earlier value is a violation.
Two clients observing operations in different orders. There is a single linearization; all observers are consistent with it. A history where client 1 sees $A$ then $B$ and client 2 sees $B$ then $A$ is not linearizable.
Serving linearizable reads from an arbitrary follower without coordination. The follower may lag, and its answer may precede a completed write. Leader leases or a quorum read are required.
Full availability during a partition while remaining linearizable. CAP, directly. A minority partition must refuse.
Does not forbid
It does not forbid reordering concurrent operations, and this is the misreading that produces bogus bug reports. If two operations overlap in real time, either order is legal. A Jepsen violation is only a violation when the operations are non-overlapping, and a “wrong” result from operations issued simultaneously by two clients is usually correct behaviour.
It does not require a global clock. The real-time order is a partial order on intervals and is only constrained where intervals do not overlap; no implementation needs synchronized clocks. Spanner uses TrueTime to get strict serializability across shards, but ZooKeeper and etcd get linearizability from a consensus log with no clock at all.
It does not require every operation to be linearizable. Systems routinely mix levels. etcd offers both linearizable reads and cheaper serializable reads on the same data, and DynamoDB has eventually consistent and strongly consistent reads as a per-request flag. The choice is per operation, not per system.
It does not imply transactional atomicity. Each operation is atomic; a
sequence of them is not. Two linearizable reads may straddle a write and see
inconsistent state. This is why Redis has MULTI and Lua scripts even though
individual commands are already linearizable.
It does not mean slow. Linearizable reads on a leader with a valid lease are local reads, no round trip. The cost appears on writes and on lease renewal, not on every read.
Boundary
- It is a safety property, not a liveness one. A system that never responds is trivially linearizable. Availability is a separate concern.
- Single objects only. Multi-object atomicity needs transactions; see T071.
- The specification must be sequential and deterministic. Objects with nondeterministic specifications need a generalization.
- The definition allows pending operations to be completed or discarded. An operation invoked but never responded to may be linearized or ignored, which is what makes histories with crashed clients analyzable.
- General checking is NP-complete, though bounded concurrency makes it practical, and this is why Jepsen limits concurrency in its test workloads.
The condition to carry: linearizability is what lets you pretend a distributed object is a variable. That pretence is bought with coordination, it is bounded by CAP, and it is the only common consistency model that composes.