What Linearizability Actually Means
Before explaining how Jepsen checks it, we need to define it precisely.
Linearizability (also called "strong consistency" or "atomic consistency") is a guarantee about concurrent operations on a shared object. It says: every operation must appear to take effect instantaneously at some point between when the client sent the request and when the client received the response. Furthermore, the order of these instantaneous effects must be consistent with real time—if operation A completes before operation B starts, then A must appear to have happened before B in the global order.
A simpler way to think about it: linearizability means the system behaves as if there is a single, correct copy of the data, even though there are actually many replicas.
Why Checking It Is Hard
Testing availability is easy: did the cluster crash? Testing correctness is hard because of the info (unknown) outcomes.
Imagine this scenario:
1. Client A sends write(x = 5). The network times out. Outcome: info.
2. Client B sends read(x). It returns 5. Outcome: ok.
3. Client C sends read(x). It returns 4. Outcome: ok.
Did Client A's write succeed or not? Client B's read suggests it did. Client C's read suggests it did not. Both reads happened after the write timed out. This is a violation—but only if the write actually succeeded. If the write silently failed, then both reads returning 4 would be fine (though Client B returning 5 would then be the violation).
The checker must explore both possibilities and determine which one (if either) produces a consistent history.
Knossos: The Linearizability Checker
Knossos is Jepsen's linearizability checker. It takes the complete History log and attempts to find one valid sequential ordering of all operations that:
1. Is consistent with the real-time ordering (completed operations before started operations)
2. Produces the correct outputs for a correct implementation of the data structure
If Knossos can find such an ordering, the history is linearizable and the test passes. If it cannot find any valid ordering after exhaustive search, it has proven the database violated linearizability, and it outputs the specific counterexample.
The Computational Cost
Linearizability checking is NP-Hard in the general case. The search space of possible orderings grows exponentially with the number of concurrent operations. Knossos uses several techniques to make this tractable:
- Wing & Gong algorithm: prunes the search space by only considering operations at their "linearization points"
- Memoization: caches already-explored states to avoid redundant work
- Early termination: stops as soon as a violation is found
For typical Jepsen test histories (hundreds to low thousands of operations), Knossos completes in seconds to minutes. For very long tests with many concurrent clients, analysis can take hours.
A common interview question at companies building databases or distributed systems is: "What's the difference between linearizability and serializability?" Linearizability is about single-object, real-time ordering (each operation appears atomic). Serializability is about multi-object transactions (a set of transactions appears to execute in some serial order, but not necessarily in real-time order). A system can be serializable but not linearizable (transactions are ordered, but stale reads are possible), or linearizable but not serializable (single-object operations are atomic, but multi-object transactions are not supported). Strict serializability is both simultaneously, and is what systems like Spanner and CockroachDB claim to provide.
Key Point: Knossos does not sample or approximate. It either finds a valid linearization (proof of correctness) or proves none exists (proof of violation). This is what makes Jepsen results so authoritative—they are mathematical proofs, not probabilistic assessments.