Linearizability
Suppose two clients hit a "replicated" bank account at nearly the same instant. Client A deposits $100. Client A then tells client B by phone, "I just deposited money — go check." Client B reads the balance a moment later. If the system is truly correct, B must see the deposit. This obligation is the essence of linearizability. Operations must behave as though they happened instantaneously at some point between their invocation and their response. Linearizability is the strongest consistency guarantee commonly used in distributed systems. Real systems care about this deeply. Distributed locks, leader election services, and configuration stores like ZooKeeper and etcd advertise linearizable operations. Consensus-backed key-value stores do too. Weaker guarantees let clients observe impossible histories. Examples include stale reads after acknowledged writes, or values that appear to go backward in time. Another example is two clients that both believe they hold the same lock. Building a distributed lock manager, a unique ID generator, or a leader-election service on a non-linearizable store is risky. It is a classic way to introduce silent correctness bugs. These bugs often surface only under load or network partition. The big picture is that linearizability gives programmers an illusion. A replicated, concurrent, network-delayed system behaves like a single copy of the data. It appears to be operated on one request at a time. This illusion is precise enough to reason about formally — it composes across objects. It is also strict enough to rule out entire classes of bugs. But it is not free. As this article's forward pointer toward the CAP Theorem will show, it costs availability during partitions. It also costs latency even when the network is healthy. This article defines linearizability precisely. It distinguishes it from weaker models such as Sequential Consistency and Eventual Consistency. It walks through the checking algorithm used to verify whether a concrete execution trace is linearizable. It also analyzes why the definition is correct, composable, and expensive. It builds directly on Replication and Consistency Models. It sets up the tradeoffs formalized by the CAP Theorem.
- Linearizability requires every operation to appear to take effect instantaneously at some point between its invocation and its response.
- It is equivalent to requiring a real-time-respecting total order over all operations that is consistent with each object's sequential specification.
- It is strictly stronger than sequential consistency: sequential consistency preserves program order but not real-time (wall-clock) order across clients.
- Linearizability is composable: if every object in a system is linearizable, the whole system is linearizable — this is why it's the workhorse guarantee for building larger systems out of smaller linearizable pieces (locks, registers, queues).
- Checking whether a given concurrent history is linearizable is decidable but NP-complete in general; the Wing-Gong / linearization-point method is the standard proof technique.
- Achieving linearizability in a replicated system requires consensus-like coordination (e.g., Paxos/Raft) and inherently sacrifices availability or latency during network partitions.
Linearizability makes a replicated object behave exactly like one atomic object where every operation happens instantly at some real point between its call and its return.
The idea
A history is a sequence of operation invocations and responses issued by concurrent clients on some set of shared objects (registers, queues, counters, locks). Each operation `op` has an invocation event `inv(op)` and a response event `res(op)`, and it spans the real-time interval `[inv(op), res(op)]`. Two operations are concurrent if their intervals overlap; otherwise one precedes the other in real time. A history `H` is linearizable if there exists a way to assign each operation a single instant — a linearization point — inside its invocation-response interval, such that: 1. Sequential legality: reading the operations off in order of their linearization points yields a sequence that is a legal execution of the object's sequential specification (e.g., a queue behaves like a FIFO queue, a register returns the last value written). 2. Real-time order preservation: if operation `A` finishes (its response) strictly before operation `B` starts (its invocation) in real time, then `A`'s linearization point must come before `B`'s. Equivalently: linearizability requires the existence of a total order `sequential consistency, introduced by Lamport for shared-memory multiprocessors. Sequential consistency also demands a legal total order consistent with each individual client's program order, but it does not require that order to respect real time across different clients. This means a sequentially consistent system can let client B, after being told "the write completed," still read a stale value — because sequential consistency only cares that B's own prior operations appear in order, not that B's read happens after A's write in wall-clock terms. Linearizability closes this gap and is therefore called a strong consistency model: it is the consistency guarantee that matches our intuition of "as if there were only one copy of the data, processed one operation at a time, in an order compatible with what clocks on the wall would show."
How it works
There are two distinct things to understand: (1) how a system achieves linearizability (the mechanism), and (2) how to check whether a given recorded history is linearizable (the verification algorithm). Both matter for a working engineer — one to build correct systems, one to test them.
Mechanism. In practice, linearizability over replicated data is achieved by funneling all operations through an agreed total order, typically via a Consensus protocol (Paxos, Raft) or a single elected leader that serializes all reads and writes. Every operation is committed to a replicated log; a client's operation only returns once its effect is durably ordered relative to all previously completed operations. Reads must also be routed through this ordering mechanism (or use a lease/quorum-read technique) — otherwise a read from a stale replica breaks real-time order preservation.
Verification. Given a recorded history of invocations and responses (e.g., from a test harness hammering a system with concurrent operations), we want to decide: is this history linearizable? The standard technique is to search for a valid linearization — a permutation of the operations that is legal under the sequential specification and respects real-time non-overlap constraints. This is exactly the algorithm underlying tools like the Knossos/Jepsen linearizability checker (based on Wing & Gong's method, later optimized by Lowe's `Wing-Gong+cache` and the `P-compositional` algorithms). ```pseudocode
# Decide whether history H (a set of operations, each with
# invocation time, response time, and arguments/return value)
# is linearizable with respect to sequential spec S. #
# Model: at any point, the "linearized state" is some prefix of
# operations already placed in the order, tracked by a bitmask
# (or a set) of which ops are "done". We search for an order of
# all n operations that is (a) legal under S and (b) respects
# real-time precedence. function IS_LINEARIZABLE(H, S): ops <- all operations in H n <- |ops| precedes <- {} # real-time partial order for A in ops: for B in ops: if A.response_time < B.invocation_time: precedes.add(A -> B) # A must be linearized before B memo <- empty hash map # memo[(state, done_set)] -> bool return SEARCH(S.initial_state(), empty_set, ops, precedes, memo) function SEARCH(state, done, ops, precedes, memo): if done == all(ops): return true key <- (state, done) if key in memo: return memo[key] for op in ops where op not in done:
# op is only eligible now if every operation required to
# precede it in real time is already done if exists p in precedes such that p -> op and p not in done: continue
# try applying op to the sequential object; it must
# return the same result it returned in the real history (new_state, expected_return) <- S.apply(state, op.arguments) if expected_return != op.actual_return: continue if SEARCH(new_state, done ∪ {op}, ops, precedes, memo): memo[key] <- true return true memo[key] <- false return false ``` This is a backtracking search over the space of "which operations have been linearized so far," pruned by two constraints: real-time precedence (an operation cannot be scheduled before something it must follow) and semantic legality (applying the object's sequential operation must reproduce the return value actually observed). The `memo` table (keyed by object state + the set of completed operations, not their order) is what makes the Wing–Gong style algorithm tractable in practice for moderate concurrency — it collapses many different orderings that reach the same state into one cache entry.
Complexity & correctness
Runtime of the checking algorithm. In the worst case there is no exploitable structure, and the search must try all consistent orderings of `n` concurrent operations. Since the state space is keyed by (object state, subset of completed operations), and object state can itself depend on the subset in complex ways, the naive bound is ``` O(n! ) — trying every total order in the worst case (no memoization benefit), ``` but with memoization keyed by `(state, done_set)` the bound improves to roughly ``` O(2^n · n · |states|) ``` because there are at most `2^n` distinct "done sets" and, from each, at most `n` operations to try next. This is still exponential, and indeed checking linearizability of a history is NP-complete in general (Gibbons & Korach, 1997) — the problem is at least as hard as Hamiltonian path style combinatorial search, because real-time constraints plus semantic legality can encode arbitrary constraint-satisfaction structure. For special object types (e.g., FIFO queues, or histories with bounded concurrency `k`), faster algorithms exist: the bounded-concurrency case can be checked in roughly `O(n^k)` time using dynamic programming over the "frontier" of pending operations, which is what production checkers like Knossos exploit — real test traces rarely have more than a handful of truly concurrent operations at once, keeping the exponent small.
Why memoization is sound. The key correctness argument for the memo table is an invariant: the legality of extending a partial linearization from state `s` with the remaining operations `R` depends only on `s` and `R`, not on the specific order used to reach `s`. This holds because the sequential specification is a function of (current state, next operation) → (new state, return value); it has no memory of which order of prior operations produced `s`, only what `s` is. Hence any two search paths that reach the same `(state, done_set)` pair have identical futures, and it is safe to cache one boolean answer for both — this is the standard "optimal substructure" argument used to justify dynamic programming.
Correctness of the definition itself (why linearizability composes). The single most important theorem about linearizability is that it is locally decidable and compositional: > Theorem (Herlihy & Wing, 1990). A history `H` over multiple objects is linearizable if and only if, for every object `x`, the sub-history `H|x` (all operations restricted to `x`) is linearizable. The proof sketch: if each per-object sub-history has a witnessing linearization order `entire set of operations (it comes from actual wall-clock intervals, which are globally consistent by definition). One can therefore take the union of all the `lack (sequential consistency is not composable: two objects individually sequentially consistent, combined, need not be sequentially consistent as a pair).
Tradeoffs, honestly. Linearizability's cost is coordination: every write (and, in the strict definition, every read) must be ordered relative to all others, which typically requires a majority Consensus round-trip or single-leader serialization. This adds latency (extra network round trips) and, under a network partition, forces the system to sacrifice availability (a minority partition must refuse operations rather than risk violating real-time order) — the precise tension that the CAP Theorem formalizes. Systems that cannot pay this cost fall back to sequential consistency, causal consistency, or eventual consistency, trading correctness guarantees for latency and availability.
Worked example
Consider a single register `R` (starting value `0`) accessed by three concurrent clients. We record the following real-time history (times are arbitrary units):
| Op | Invoke | Respond | Action | Return |
|---|---|---|---|---|
| A | 0 | 5 | write(R, 1) | ok |
| B | 3 | 8 | write(R, 2) | ok |
| C | 6 | 10 | read(R) | 2 |
| D | 9 | 12 | read(R) | 1 |
Is this history linearizable? Apply the real-time constraints: `A` ends at 5, `B` starts at 3 — they overlap, so no ordering constraint between A and B from real time alone. `B` ends at 8, `C` starts at 6 — overlap, no constraint. `C` ends at 10, `D` starts at 9 — overlap, no constraint. But `A` ends at 5, and `D` starts at 9 — no overlap, so `A` must be linearized before `D`. Similarly `A` ends at 5, `C` starts at 6 — no overlap, so `A does not force `B is forced too!). So both writes must precede `D`, meaning `D` must also read `2`. But `D` actually returned `1`.
Conclusion: this history is not linearizable. No legal total order respecting real-time constraints can make `D` see `1`, because both writes are real-time-ordered before `D` starts, and the sequential register spec says a read must return the most recently written value in the linearization order — which under any valid order is `2`. The trace exhibits a "stale read after a real-time-ordered write," exactly the anomaly linearizability is designed to forbid. If instead the history had `D`'s invocation overlap with `B`'s interval (say `D` invoked at time 4), the constraint `B
Common pitfalls & traps
| Pitfall | Why it happens | Fix |
|---|---|---|
| Confusing linearizability with sequential consistency | Both require a legal total order consistent with program order; only linearizability adds the real-time constraint | Always ask: does the order need to respect wall-clock precedence across clients, or just each client's own order? |
| Treating "eventually consistent, replicated" stores as linearizable for locks | Async replication means a client can read a stale replica after a write is acknowledged elsewhere | Route all lock/CAS operations through a consensus-backed leader or quorum reads/writes |
| Forgetting that reads must also be linearized | Engineers often serialize writes carefully via consensus but let reads hit any replica for speed | Use quorum reads, leader reads, or lease-based reads that guarantee freshness |
| Assuming linearizability composes for "systems" built from non-linearizable parts | The composition theorem only holds when each individual object is linearizable | Verify per-object linearizability before relying on system-level correctness |
| Ignoring the exponential cost of checking real histories | Testing tools naively enumerate all `n!` orderings | Use memoized/bounded-concurrency algorithms (Wing–Gong with caching, or Lowe's optimizations) |
Pioneers & history
Origins · 1 minMaurice Herlihy and how this was discovered
Where this matters
Coordination services — ZooKeeper, etcd, Consul, Chubby — advertise linearizable writes (and often linearizable reads via quorum or leader leases) because they back distributed locks, leader election, and configuration management, where a stale or reordered view causes split-brain bugs. Consensus-replicated databases such as Spanner, CockroachDB, and FoundationDB provide linearizable (or externally consistent) single-key operations as a building block for stronger transactional guarantees. Hardware memory models and lock-free data structure libraries use linearizability as the correctness condition for individual objects (queues, stacks, counters) implemented with atomic compare-and-swap instructions — the same Herlihy–Wing framework applies whether the "replicas" are network nodes or CPU cache lines. Testing tools like Jepsen run adversarial network-partition experiments against production databases and use linearizability checkers to catch violations that vendors' own test suites miss, directly reusing the Wing–Gong search algorithm described above. This is also precisely the guarantee whose cost — coordination during partitions — feeds into the tradeoffs described by the CAP Theorem, and whose weaker cousins (Sequential Consistency, Causal Consistency, Eventual Consistency) trade real-time guarantees for availability and latency.
Ask the tutor: How does the CAP theorem formally connect to the availability cost of enforcing linearizability during a network partition?
Is linearizability the same as "strong consistency"?
"Strong consistency" is an informal umbrella term, and linearizability is its most common precise instantiation, but not the only one. Some authors use "strong consistency" loosely to mean anything stronger than eventual consistency, which can include sequential consistency or even snapshot isolation in database contexts. Linearizability specifically adds the real-time constraint on top of sequential legality, making it the strictest single-object consistency model in common use. When precision matters — for instance, in a paper or a system's formal spec — it's best to name the exact model (linearizability, sequential consistency, causal consistency) rather than rely on "strong consistency," since the real-time guarantee is exactly what differentiates the strongest tier from the merely-ordered ones.
Does linearizability require operations to be truly instantaneous?
No — real operations always take nonzero time (invocation to response), and linearizability only requires that there exists a single point within that interval where the operation can be considered to have "taken effect" for the purposes of ordering. Physically, no operation is instantaneous; linearizability is a specification technique, not a claim about physics. What matters is that some consistent choice of such points, one per operation, produces a legal, real-time-respecting total order. This is why it's called an "atomicity" property: the operation, despite spanning real time, behaves indivisibly, as if it happened at one instant.
Why is linearizability expensive, and how do systems avoid paying the cost everywhere?
Linearizability requires every operation to be ordered relative to every other operation across the whole system in real time, which typically demands consensus or a single serializing leader — adding network round-trips and reducing availability during partitions. Systems avoid this cost by scoping linearizability narrowly: for example, only compare-and-swap operations on a lock key go through consensus, while high-volume reads of non-critical data use faster, weaker consistency (eventual or causal). Some systems offer "linearizable reads" as an opt-in, expensive path (quorum read or leader read) alongside cheap stale reads, letting the application choose per-operation which guarantee it needs.
How does linearizability relate to serializability in databases?
They are related but orthogonal: linearizability is about the real-time ordering of individual operations on objects (registers, locks), while serializability is about transactions — groups of operations across possibly many objects — appearing to execute in some serial (not necessarily real-time-respecting) order. Strict serializability is the transactional analog that adds linearizability's real-time constraint to serializability, making it the strongest transactional guarantee. A system can be serializable without being linearizable (e.g., if transaction order doesn't respect wall-clock precedence), and a linearizable single-object store doesn't automatically give you multi-object transactional isolation.
Can a system be linearizable without using consensus (Paxos/Raft)?
In principle yes, if there is a single non-replicated authority handling all operations — a lone server trivially satisfies linearizability because there's only one copy and one order of execution. The hard case is when data is replicated for fault tolerance; then some coordination mechanism must ensure all replicas agree on an order, and in practice this mechanism is consensus or an equivalent (e.g., a single elected leader with fencing tokens, or synchronized clocks with bounded uncertainty as in Google Spanner's TrueTime). Without such coordination, replicas can diverge or serve stale reads, breaking linearizability whenever a client observes a real-time-ordered pair of operations across replicas.
Why is checking linearizability NP-complete, intuitively?
Deciding whether a recorded history is linearizable amounts to searching for one valid total order among the concurrent operations, where "valid" combines two kinds of constraints: real-time precedence (a partial order) and semantic legality (does replaying operations in this order reproduce every observed return value?). This combination can encode hard combinatorial constraint-satisfaction problems — Gibbons and Korach showed a reduction establishing NP-completeness in general. In practice, real test histories have limited concurrency (few overlapping operations at once), so bounded-concurrency algorithms with polynomial complexity in the bound, plus memoization, make checking tractable for realistic traces even though the worst case is intractable.
What is the simplest example of a non-linearizable but still "useful" consistency model?
Sequential consistency is the classic example: it requires a legal total order consistent with each client's own program order, but drops the real-time cross-client constraint. This is weaker but cheaper, and it matches older shared-memory multiprocessor hardware models where enforcing real-time order across cores was considered too costly. Causal consistency is another practical middle ground: it only requires causally related operations (one that "happens after" seeing another's effect) to be ordered consistently, letting unrelated concurrent operations be seen in different orders by different observers, at much lower coordination cost than linearizability.