Linearizability

Linearizability is a correctness condition for concurrent objects, defined formally by Maurice Herlihy and Jeannette Wing in 1990. Martin Kleppmann calls the formal definition not entirely straightforward and gives the key idea informally please-stop-calling-databases-cp-or-ap:

If operation B started after operation A successfully completed, then operation B must see the system in the same state as it was on completion of operation A, or a newer state.

This is what "consistency" means in the CAP theorem. It has nothing to do with the C in ACID.

What it forbids

Kleppmann's example is the 2014 World Cup final. Alice and Bob are in the same room. Just after the final score is announced, Alice refreshes, sees the result and tells Bob. Bob reloads, his request lands on a lagging replica, and his phone says the match is still going. If they had reloaded at the same moment, different answers would be unsurprising, because neither knows exactly when the server processed each request. But Bob started his request after hearing Alice, so he expects a result at least as recent as hers, and the stale answer violates linearizability.

What established the order was a channel outside the system: Alice's voice. Without it Bob would never have known his result was stale. A database can't know what backchannels its clients have, so a database that promises linearizability has to look as though there is a single copy of the data, even when copies sit in replicas and caches in several places.

Why it costs

Making many copies look like one takes coordination, which is expensive. Kleppmann's sharpest illustration is that a CPU doesn't provide linearizable access to local RAM: on modern processors an explicit memory barrier instruction is needed to get it, and he cites the x86-TSO model by Sewell et al. for the details. Even testing whether a system is linearizable is hard; he points to Kyle Kingsbury's Knossos checker.

So systems give it up on purpose. Databases with snapshot isolation or MVCC are intentionally non-linearizable, because enforcing it would reduce the concurrency they can offer. ZooKeeper serves reads from whichever server a client is connected to, which is fast and not linearizable, and lets a client issue sync before a read to get a linearizable read at a performance cost. Across a network partition the CAP argument applies: a replicated system has to give up linearizability or stop serving on one side of the split.

What it is not

Serializability is a guarantee about transactions, and linearizability is a guarantee about the recency of individual operations; neither implies the other. Kleppmann's example is PostgreSQL's serializable snapshot isolation, which provides serializability and not linearizability. Quorum reads and writes with R + W > N are sometimes said to be linearizable, and he advises against relying on that, because sloppy quorums and read repair create edge cases that break the quorum condition. A consensus protocol underneath doesn't make reads linearizable by itself either, which is the ZooKeeper case.

Getting it in practice

Systems that need it route operations through something that fixes their order. meerkat-introduction puts linearizability first among Cloudflare's requirements, so that service authors can reason about the cluster the way they reason about local memory on a single thread. Meerkat sends reads through its consensus log: a replica that proposes a read at a slot already decided for a write is forced to learn that write and re-propose the read after it, and a replica that can't reach a majority fails the read instead of answering stale. The same page notes that Raft achieves linearizable reads served by the leader by using leases. distributed-consensus covers the algorithms themselves.

On one machine the question turns into one about memory models. shared-memory-consistency-causality builds a deliberately unhelpful multiprocessor to work out what ordering atomic instructions must guarantee. cobaltc's specification defines a happens-before relation for its threads and states explicitly that this relation doesn't require a machine-level memory fence for every ordering edge. art-of-multiprocessor-programming is the textbook treatment of linearizability for concurrent data structures.

Connections

• stop-calling-databases-cp-or-ap — Kleppmann's case that CP and AP misdescribe real databases, built on how strict CAP's linearizability requirement is
• ability-guarantee-tradeoff — linearizability as a guarantee paid for with concurrency or latency