From sets to linearizability checks
Jepsen's original tests worked against a simple abstraction: each client added integers from a disjoint sequence into a shared set stored in the database, then performed a final read to verify that every successful write was present. That model worked well for eventually-consistent, AP-style systems like Riak, where unordered set membership is the natural semantic. To exercise a linearizable system, Jepsen implemented set addition as a compare-and-set operation, replacing the old set with the current value plus the new number. A successful CAS should guarantee the element appears in the final read.
This approach verified sequential consistency to some degree, and linearizability only in limited scenarios. A database could legally delay visibility of writes as long as they became visible before the final read. The test could not exercise operations other than CAS, such as deletions, and offered no way to validate systems like mutexes, queues, or semaphores. Worse, when a test failed, it was unclear which operation caused the failure—was it a specific CAS, or some later operation that obliterated the effects of an earlier write? The need for a checker that could handle arbitrary operations and explain precisely why a history failed to linearize led to the design of Knossos, a model checker applicable to both formal specifications and opaque real-world databases.
Representing a model as state and step
Linearizability, like sequential consistency, demands that every operation appear to take effect atomically in some total order, between its invocation and its completion. That means there is always a single "true" system state at any moment. Knossos therefore models any linearizable system as a state plus a function, step, which takes the current state and an operation and returns the new state.
In Clojure this is expressed via a protocol called Model. Consider a mutex with two possible operations, :acquire and :release, and a boolean state locked?. Locking an unlocked mutex returns a new state with locked? set to true. Locking an already-locked mutex returns a special inconsistent state—a marker that the model forbids this sequence of operations. To check a single-threaded history, Knossos reduces step over the initial state and the operation list; if the result is inconsistent, the history is invalid.
Ambiguity in concurrent histories
Real histories are not single-threaded. They consist of pairs of :invoke messages followed by :ok, :fail, or :info results. An :ok means the operation succeeded; :fail means it definitely did not take effect; :info means the outcome is unknown, perhaps because of a timeout or an indeterminate server response. A hung operation may take effect at any time in the future, making it concurrent with every later operation.
The check becomes a search: find some total order of the operations, respecting each operation's invocation and completion times, such that reducing step over that order never produces an inconsistent state. For \(n\) concurrent operations, the number of candidate interleavings is \(O(n!)\), which quickly becomes intractable.
State deduplication
The first optimization exploits a key property of the model: whether an operation is valid depends solely on the current state, not on the history that produced it. If two registers both hold the value 2, applying the same operation to either yields an equivalent result. Knossos cannot perform symmetry reduction based on the structure of step, because it knows nothing about the system's internals. But it can detect when the search returns to the same state with the same pending set of operations, and drop all but one such world. This collapses interchangeable orders—concurrent reads, or writes that land on the same value—dramatically shrinking the search space. Knossos keeps a cache of visited worlds and avoids revisiting them.
Lazy exploration with worlds
The search seeks any valid linearization, not every one. Knossos therefore prioritizes branches that seem cheapest to explore, deferring harder ones. This is not breadth-first or depth-first, but a heuristic guided by branching factor. The exploration state is an immutable data structure called a world, which carries three components:
- A fixed history: the sequence of operations already ordered in this possible universe.
- A current model state resulting from reducing
stepover the fixed history. - A set of pending operations—those invoked but not yet applied.
For example, a world might have a fixed history of lock, unlock, lock, a model state where the mutex is locked, and a second lock attempt pending. A newly arriving unlock could allow that pending lock to complete. A single pure function takes a world and returns a set of successor worlds, making the entire search process a stateless transformation over data structures.
Parallel work stealing
Because worlds are immutable and the exploration function is pure, the search parallelizes trivially. Early versions of Knossos performed a breadth-first walk, reducing each history index across all outstanding worlds in parallel. That approach has a serious flaw: it locks the search into breadth-first order, preventing the algorithm from diving down promising paths first.
The current design uses multiple explorer threads, each consuming worlds from a priority queue sorted by estimated exploration difficulty. As a thread discovers successor worlds, it inserts them back into the pool. If any thread finds a world that encompasses every operation in the history, the history is proven linearizable. The shared priority queue—a java.util.concurrent.BlockingPriorityQueue—is a synchronization bottleneck, so Knossos stripes the queue into several subqueues with thread affinity. Each thread prefers its own queue, reducing lock contention; when a thread exhausts its local work, it steals from neighbors.
This work-stealing approach trades memory locality for parallelism. Moving worlds through queues pushes them out of CPU cache. The granularity of work—how far a thread pursues a given world before returning to the pool—is a tunable parameter: too coarse and threads starve; too fine and synchronization and cache-miss overhead dominates.
Path compression for concurrent states
Knossos inherits an important trick from speculative execution research: memoization over world states. Margo Seltzer's 2013 RICON East talk framed x86 execution as a massive function that maps a vector of registers and memory to a subsequent state. If you can compress that state space and predict which regions of memory are untouched by a computation, you can cache partial results and skip over equivalent future executions.
The insight carries over to linearizability checking. Most parallel workloads touch only a slice of memory at any instant — an increment loop like for(i = 0; i < 100; i++) { arr[i]++ } modifies one element at a time and leaves the rest of memory degenerate. Knossos's state space has the same property: fixed histories can be collapsed whenever the model state and pending operation set match. Combined with its lazy, multiverse-style execution — where operations are explored from many points simultaneously — that degeneracy makes memoization viable. When a search lands on an already-visited world, Knossos aborts the branch entirely. It doesn't cache results, only the fact that a world was reached.
The mechanism resembles a group traversing a maze together: when one explorer hits a dead end, they mark that path so nobody else re-traces it. At branch points, only unexplored paths get taken. The check is nondeterministic but requires no locks, keeping it cheap. Cache hit rates run low, but every hit eliminates an exponential cloud of descendant worlds, which is where the runtime savings accumulate.
Immutable worlds, mutable frontiers
Exploration produces combinatorial branching. Two concurrent writes a and b force the checker to visit [], [a], [b], [a b], and [b a]; each of those worlds forks into hundreds, then millions, of successors, demanding an enormous number of copies.
Haskell's persistent data structures and parallel pure-function execution would make a natural fit here, but Knossos takes a Clojure route instead. The consistency model is written as a pure function over immutable maps, vectors, and sets. Forking a world into variants does not copy the entire state: Clojure's structural sharing stores only a delta atop a reference to the original. This makes forking millions of worlds tractable.
The immutable core allows worlds and the pure exploration functions to be passed freely across threads, enabling both parallel execution and the memoization cache. But the search driver itself needs mutable state: a priority queue of unexplored worlds at the search frontier, the memoizing cache shared between threads, and bookkeeping atoms to track search progress and cache size. Knossos layers these on as a striped java.util.concurrent.PriorityQueue, a concurrent hashmap for memoization, Clojure atoms, and Java CAS-based atomics. This is the most fragile part of the system — its behavior is deliberately nondeterministic, trading inter-core synchronization for traversal freedom.
The payoff from minimized synchronization came from a 24-core (48 HT) Xeon with 128GB of ECC memory, funded by a Comcast research grant for Jepsen. Profiling with Yourkit exposed lock and CAS contention that capped scalability at roughly four cores; removing nearly all thread stalls raised performance by two orders of magnitude. Knossos can now check 5-process histories of 150–200 elements in minutes rather than days.
Notable optimizations remain unexplored — such as detecting crashed processes and optimistically inserting a world where a failed process never executes its operation — but current Knossos is enough to find linearization errors in real-world histories. Next on the list: RabbitMQ.
