Not only is this system impossible to build, but even if it were possible, it would not be linearizable.The source of that quote was a strong—and correct—claim about the hypothetical coordinator design. But making that specific point doesn't solve the bigger problem. It's unlikely to be the last time such a scheme is proposed, and manually auditing every algorithm is unsustainable. The goal is to raise the level of analysis around these systems.
A More Precise Definition of "Linearizable"
To prove something is broken (or correct), we must first define what "correct" means. In Knossos, we analyze a system's history—a sequence of operations performed by logical threads. Each operation has an invocation (marked with:invoke) and a completion (marked with :ok). The operation type is described by :f, and its specific value is contained in :value.
[{:process :c2, :type :invoke, :f :write, :value 850919}
{:process :c1, :type :ok, :f :write, :value 850914}
{:process :c1, :type :invoke, :f :read, :value 850919}
{:process :c1, :type :ok, :f :read, :value 850919}]
knossos.core/step function, validates whether a single operation is legal when applied to a specific state. For example, a register model enforces that a read should return the most recently written value. If an operation is invalid for a given state (e.g., reading a 5 when the register is nil), step throws an error.
Consider the evaluation of [b a] from a concurrent history of "write 5" (a) and "read 5" (b) on a register initially set to nil. This sequence is invalid because we cannot get the value 5 from nil.
From these primitive operations, we can reduce a sequence of events to a final state if they are valid.
user=> (reduce step
(Register. 0)
[{:process :c1, :type :ok, :f :write, :value 4}
{:process :c2, :type :ok, :f :read, :value 4}]
#knossos.core.Register{:value 4}
user=> (reduce step
(Register. 0)
[{:process :c1, :type :ok, :f :write, :value 4}
{:process :c2, :type :ok, :f :read, :value 7}])
RuntimeException read 7 from register 4 knossos.core.Register (core.clj:43)
A Paradox: Multiplying the Problem to Solve It
The naive approach to finding a linearization—literally enumerating every possible interleaving and subset of operations—fails at scale. Even with just 10 concurrent operations, the space explodes exponentially, making exhaustive testing impractical beyond roughly 12 to 16 operations. This brute-force strategy, as used by tools like Microsoft Research's PARAGLIDER, is not a general solution. To make the search tractable, we need to think differently. Rather than computing permutations from scratch, we use the model to prune the search space early. This involves a seemingly counterintuitive step: making the problem even harder by multiplying the state space. Given a history of four invocations, which we'll calla, b, c, and d:
[a b c d]
[]
[a]
[a b]
[a b c]
[a b c d]
[b a] cannot succeed—then any longer history containing that prefix ([b a c] or [b c a]) is also invalid. We don't need to test them.
This recursive principle dramatically reduces what we must compute.
[]
[a]
[b]
[a b]
[b a]
Why This Helps
By using the model to check each new operation as it's appended, we fail fast. If the model cannot process a new operation within any of the current "worlds" (the active set of possible histories), that world is pruned immediately. This stops us from exploring any of its potentially massive subtrees of futures. When a read operation returns with an actual value, for instance, it doesn't merely test one path—it eliminates every concurrent history that would implicitly contradict that read. Knossos uses Clojure's immutable data structures to hold this search state, representing multiple worlds as a set of consistent linearized histories. Each invocation splits the possibilities, and each completion constrains them. This strategy pushes the boundary of what we can test, allowing us to check much larger histories for correctness in practice. With tools like this, we can trade he-said-she-said arguments for empirical—and reproducible—verification.What the model looks like in code
To test a model properly, we need an unambiguous description that a computer can run. Antirez's proposal is simple enough to formalize: a node is a Clojure structure holding its state, replication offset, and knowledge of its peers, while things like "the WAIT command relies on the node knowing the replication offsets of its peers" become plain fields in that structure.
(defn node
"A node consists of a register, a primary it replicates from, whether it is
isolated from all other nodes, a local replication offset, and a map of node
names to known replication offsets."
[name]
{:name name
:register nil
:primary nil
:isolated false
:offset 0
:offsets {}})
The proposal leans heavily on immutable, pure systems—Clojure, Erlang, ML, and Haskell fit naturally. Keeping the code immutable, even if you're writing in Ruby or Java, pays off later when you need to reason about histories.
(defn client
"A client is a singlethreaded process which can, at any time, have at most
one request in-flight to the cluster. It has a primary that it uses for reads
and writes, and an in-flight request.
Clients can be waiting for a response, in which case :wait will be the
replication offset from the primary they're awaiting. :waiting is the value
they're waiting for, if conducting a write."
[name]
{:name name
:node nil
:writing nil
:waiting nil})
A coordinator is even simpler. It exists to pick failover targets and knows who the current master is.
(defn coordinator
"A controller is an FSM which manages the election process for nodes. It
comprises a state (the phase of the election cycle it's in), and the current
primary."
[primary]
{:state :normal
:primary primary})
Putting nodes and coordinator together into a full system requires translating prose like "when we start A is the master" into concrete state. That means choosing the first node as the primary and making sure that fact is reflected everywhere it matters.
(defn system
"A system is comprised of a collection of nodes, a collection of clients, and
a coordinator; plus a *history*, which is the set of operations we're
verifying is linearizable."
[]
(let [node-names [:n1 :n2 :n3]
nodes (->> node-names
(map node)
; Fill in offset maps
(map (fn [node]
(->> node-names
(remove #{(:name node)})
(reduce #(assoc %1 %2 0) {})
(assoc node :offsets)))))
; Initial primary/secondary state
[primary & secondaries] nodes
nodes (cons primary
(map #(assoc % :primary (:name primary))
secondaries))
; Construct a map of node names to nodes
nodes (->> nodes
(map (juxt :name identity))
(into {}))
; Construct clients
clients (->> [:c1 :c2]
(map client)
(map #(assoc % :node (:name primary)))
(map (juxt :name identity))
(into {}))]
{:coordinator (coordinator (:name primary))
:clients clients
:nodes nodes
:history []}))
We also track a history of operations for every state—the same history the linearizability checker will later inspect.
Transitions: clients, writes, and reads
Writes have two phases: an invocation and a response implemented with WAIT. The client-write function encodes several constraints at once: clients are single-threaded and can't start a write while waiting for another reply, and clients must be connected to a node that is neither isolated nor mistaken about being a primary. That last check assumes a false linearization point—in reality, it's not guaranteed to be instantaneous. The model is being deliberately generous.
(def write-state (atom 0))
(defn client-write
"A client can send a write operation to a node."
[system]
(->> system
clients
(filter free-client?)
(filter (partial valid-client? system))
(map (fn [client]
(let [; Pick a value to write
value (swap! write-state inc)
; Find the node name for this client
node (:node client)
; And the new offset.
offset (inc (get-in system [:nodes node :offset]))]
(-> system
(assoc-in [:nodes node :register] value)
(assoc-in [:nodes node :offset] offset)
(assoc-in [:clients (:name client) :waiting] offset)
(assoc-in [:clients (:name client) :writing] value)
(log (invoke-op (:name client) :write value))))))))
For each eligible client, we generate a unique value to write, set the primary's register to it, bump the primary's offset, and leave the client waiting for that offset to be acked by a majority. The history records the invocation with the value written.
Completion happens only when the client's primary sees that a majority of nodes have acknowledged the target offset. Not every write can complete; the transition is gated on client state, node connectivity, and the offset map.
(defn client-write-complete
"A reachable primary node can inform a client that its desired replication
offset has been reached."
[system]
(->> system
clients
(remove free-client?)
(filter (partial valid-client? system))
(keep (fn [client]
(let [offset (-> system
:nodes
(get (:node client))
majority-acked-offset)]
(when (<= (:waiting client) offset)
(-> system
(assoc-in [:clients (:name client) :waiting] nil)
(assoc-in [:clients (:name client) :writing] nil)
(log (ok-op (:name client)
:write
(:writing client))))))))))
Reads get the same generous treatment as writes, but with a shortcut: a read is treated as a linearization point itself and happens in a single instantaneous step, adding both invocation and completion to the log at once.
(defn client-read
"A client can read a value from its node, if primary and reachable. Reads are
instantaneous."
[system]
(->> system
clients
(filter free-client?)
(filter (partial valid-client? system))
(map (fn [client]
(let [node (:node client)
value (get-in system [:nodes node :register])]
(-> system
(log (invoke-op (:name client) :read nil))
(log (ok-op (:name client) :read value))))))))
Replication and ack flow
Redis replication is broken into two instantaneous phases in the model: a node with a primary copies register state and offset, and then the primary's offset cache is updated in the reverse direction. Both phases assume connectivity and treat the primary's oplog as atomically applied—again, more generous than the real asynchronous system.
(defn replicate-from-primary
"A node can copy the state of its current primary, if the primary is
reachable."
[system]
(->> system
nodes
(remove :isolated)
(keep (fn [node]
(when-let [primary (get-node system (:primary node))]
(when-not (:isolated primary)
(-> system
(assoc-in [:nodes (:name node) :register]
(:register primary))
(assoc-in [:nodes (:name node) :offset]
(:offset primary))
(log (op (:name node)
:info
:replicate-from-primary
(:primary node))))))))))
(defn ack-offset-to-primary
"A node can inform its current primary of its offset, if the primary is
reachable."
[system]
(->> system
nodes
(remove :isolated)
(keep (fn [node]
(when-let [primary (get-node system (:primary node))]
(when-not (:isolated primary)
(-> system
(assoc-in [:nodes
(:primary node)
:offsets
(:name node)]
(:offset node))
(log (op (:name node)
:info
:ack-offset-to-primary
(:primary node))))))))))
Splitting the network, picking a master
The failover algorithm's four steps map to four functions, each gated on the coordinator having completed the previous step. Step one isolates the current master by flipping its partitioned flag directly—an act that's impossible in an asynchronous network, since it modifies state instead of sending a message. The model just assumes instant message propagation.
(defn failover-1-isolate
"If the coordinator is in normal mode, initiates failover by isolating the
current primary."
[system]
(let [coord (:coordinator system)]
(when (= :normal (:state coord))
(-> system
(assoc-in [:coordinator :state] :isolated)
(assoc-in [:coordinator :primary] nil)
(assoc-in [:nodes (:primary coord) :isolated] true)
(log (op :coord :info :failover-1-isolate (:primary coord)))))))
Step two selects a new primary from the reachable majority, choosing the node with the highest replication offset. The translation is mechanical, and again assumes the impossible.
(defn failover-2-select
"If the coordinator has isolated the old primary, selects a new primary by
choosing the reachable node with the highest offset."
[system]
(let [coord (:coordinator system)]
(when (= :isolated (:state coord))
(let [candidates (->> system nodes (remove :isolated))]
; Gotta reach a majority
(when (<= (inc (Math/floor (/ (count (nodes system)) 2)))
(count candidates))
(let [primary (:name (apply max-key :offset candidates))]
(-> system
(assoc-in [:coordinator :state] :selected)
(assoc-in [:coordinator :primary] primary)
(log (op :coord :info :failover-2-select primary)))))))))
Steps three and four broadcast the new primary's identity to slaves and clients. Each is a single atomic transition, creating another false point of linearization.
(defn failover-3-inform-nodes
"If the coordinator has selected a new primary, broadcasts that primary to
all reachable nodes."
[system]
(let [coord (:coordinator system)
primary (:primary coord)]
(when (= :selected (:state coord))
(-> system
(assoc-in [:coordinator :state] :informed-nodes)
(assoc :nodes (->> system
:nodes
(map (fn [ [name node] ]
[name
(cond
; If the node is isolated, state is
; unchanged.
(:isolated node)
node
; If this is the new primary node, make
; it a primary.
(= primary name)
(assoc node :primary nil)
; Otherwise, set the primary.
:else
(assoc node :primary primary))]))
(into {})))
(log (op :coord :info :failover-3-inform-nodes primary))))))
(defn failover-4-inform-clients
"If the coordinator has informed all nodes of the new primary, update all
client primaries."
[system]
(let [coord (:coordinator system)
primary (:primary coord)]
(when (= :informed-nodes (:state coord))
(-> system
(assoc-in [:coordinator :state] :normal)
(assoc :clients (->> system
:clients
(map (fn [ [name client] ]
[name
(assoc client :node primary)]))
(into {})))
(log (op :coord :info :failover-4-inform-clients primary))))))
With a magically sequential coordinator, only one failover transition can ever fire at a time.
(defn failover
"All four failover stages combined."
[system]
(when-let [system' (or (failover-1-isolate system)
(failover-2-select system)
(failover-3-inform-nodes system)
(failover-4-inform-clients system))]
(list system')))
Dead nodes stay dead
Antirez's proposal says a reappearing master or slaves that reconnect after partitions heal should understand who the new master is. That part is hard to interpret safely, so the model omits resurrection entirely: once a node is partitioned or fails, it never comes back. Allowing recovery would only make the system more dangerous.
All of these transitions are collected into a single step function that enumerates every legal move from a given system state.
(defn step
"All systems reachable in a single step from a given system."
[system]
(concat (client-write system)
(client-write-complete system)
(client-read system)
(replicate-from-primary system)
(ack-offset-to-primary system)
(failover system)))
Starting with a basic three-node system, where :n1 is the primary and two clients are connected, we can start taking steps.
user=> (use 'knossos.redis)
nil
user=> (-> (system) pprint)
{:coordinator {:state :normal, :primary :n1},
:clients
{:c1 {:name :c1, :node :n1, :writing nil, :waiting nil},
:c2 {:name :c2, :node :n1, :writing nil, :waiting nil}},
:nodes
{:n1
{:name :n1,
:register nil,
:primary nil,
:isolated false,
:offset 0,
:offsets {:n3 0, :n2 0}},
:n2
{:name :n2,
:register nil,
:primary :n1,
:isolated false,
:offset 0,
:offsets {:n3 0, :n1 0}},
:n3
{:name :n3,
:register nil,
:primary :n1,
:isolated false,
:offset 0,
:offsets {:n2 0, :n1 0}}},
:history []}
A write to that system returns two possible outcomes—either client :c1 or :c2 initiates. Choosing randomly, one possibility has :c2 writing value 10 to :n1, leaving the client waiting for offset 1 to be acknowledged. The primary has the write; the replicas don't yet. The history shows the invocation but not the completion.
user=> (-> (system) client-write rand-nth pprint)
{:coordinator {:state :normal, :primary :n1},
:clients
{:c1 {:name :c1, :node :n1, :writing nil, :waiting nil},
:c2 {:name :c2, :node :n1, :writing 10, :waiting 1}},
:nodes
{:n1
{:name :n1,
:register 10,
:primary nil,
:isolated false,
:offset 1,
:offsets {:n3 0, :n2 0}},
:n2
{:name :n2,
:register nil,
:primary :n1,
:isolated false,
:offset 0,
:offsets {:n3 0, :n1 0}},
:n3
{:name :n3,
:register nil,
:primary :n1,
:isolated false,
:offset 0,
:offsets {:n2 0, :n1 0}}},
:history [{:process :c2, :type :invoke, :f :write, :value 10}]}
Trying to complete that write immediately fails. There are no possible worlds where it completes, because the primary's replication offset hasn't reached the acked majority. This is the point of WAIT—writes aren't complete until acknowledged.
user=> (-> (system) client-write rand-nth client-write-complete pprint)
()
A successful write, by contrast, happens only after enough nodes have caught up. In one trajectory, value 15 lands on both :n1 and :n2, the offset map on the primary is updated, and the client's WAIT resolves. The history now records both invocation and completion.
user=> (-> (system)
client-write rand-nth
replicate-from-primary first
ack-offset-to-primary first
client-write-complete
pprint)
({:coordinator {:state :normal, :primary :n1},
:clients
{:c1 {:name :c1, :node :n1, :writing nil, :waiting nil},
:c2 {:name :c2, :node :n1, :writing nil, :waiting nil}},
:nodes
{:n1
{:name :n1,
:register 15,
:primary nil,
:isolated false,
:offset 1,
:offsets {:n3 0, :n2 1}},
:n2
{:name :n2,
:register 15,
:primary :n1,
:isolated false,
:offset 1,
:offsets {:n3 0, :n1 0}},
:n3
{:name :n3,
:register nil,
:primary :n1,
:isolated false,
:offset 0,
:offsets {:n2 0, :n1 0}}},
:history
[{:process :c1, :type :invoke, :f :write, :value 15}
{:process :n2, :type :info, :f :replicate-from-primary, :value :n1}
{:process :n2, :type :info, :f :ack-offset-to-primary, :value :n1}
{:process :c1, :type :ok, :f :write, :value 15}]})
Random trajectories through the state space are then generated by repeatedly choosing between all possible step outcomes. Because nodes never come back, the system can dead-end; in that case, we return the terminal state.
(defn trajectory
"Returns a system from a randomized trajectory, `depth` steps away from the
given system."
[system depth]
(if (zero? depth)
system
(let [possibilities (step system)]
(if (empty? possibilities)
; Dead end
system
; Descend
(recur (rand-nth possibilities)
(dec depth))))))
Running the checker
To find the interesting failures, we want to stop at the point where things go wrong. The linearizable-prefix helper finds the longest prefix of a history that's still linearizable, which pinpoints exactly where consistency breaks down.
(defn print-system
[system history]
(let [linearizable (linearizable-prefix (->Register nil) history)]
(locking *out*
(println "\n\n### No linearizable history for system ###\n")
(pprint (dissoc system :history))
(println "\nHistory:\n")
(pprint linearizable)
(println "\nUnable to linearize past this point!\n")
(pprint (drop (count linearizable) history)))))
Sampling random trajectories of 15 steps and filtering for any with nonlinearizable histories yields the verdict.
(deftest redis-test
(dothreads [i 4] ; hi haters
(dotimes [i 10000]
(let [system (trajectory (system) 15)]
; Is this system linearizable?
(let [history (complete (:history system))
linears (linearizations (->Register nil) history)]
(when (empty? linears)
(print-system system history))
(is (not (empty? linears)))))))
And the model Antirez proposed fails the test.
$ lein test knossos.redis-test
### No linearizable history for system ###
{:coordinator {:state :normal, :primary :n2},
:clients
{:c1 {:name :c1, :node :n2, :writing nil, :waiting nil},
:c2 {:name :c2, :node :n2, :writing 9, :waiting 2}},
:nodes
{:n1
{:name :n1,
:register 9,
:primary nil,
:isolated true,
:offset 2,
:offsets {:n3 0, :n2 1}},
:n2
{:name :n2,
:register 5,
:primary nil,
:isolated false,
:offset 1,
:offsets {:n3 0, :n1 0}},
:n3
{:name :n3,
:register nil,
:primary :n2,
:isolated false,
:offset 0,
:offsets {:n2 0, :n1 0}}}}
History:
[{:process :c2, :type :invoke, :f :write, :value 5}
{:process :n2, :type :info, :f :replicate-from-primary, :value :n1}
{:process :n2, :type :info, :f :ack-offset-to-primary, :value :n1}
{:process :c2, :type :ok, :f :write, :value 5}
{:process :n2, :type :info, :f :replicate-from-primary, :value :n1}
{:process :c2, :type :invoke, :f :write, :value 9}
{:process :n3, :type :info, :f :ack-offset-to-primary, :value :n1}
{:process :c1, :type :invoke, :f :read, :value 9}
{:process :c1, :type :ok, :f :read, :value 9}
{:process :coord, :type :info, :f :failover-1-isolate, :value :n1}
{:process :coord, :type :info, :f :failover-2-select, :value :n2}
{:process :coord,
:type :info,
:f :failover-3-inform-nodes,
:value :n2}
{:process :coord,
:type :info,
:f :failover-4-inform-clients,
:value :n2}
{:process :n3, :type :info, :f :ack-offset-to-primary, :value :n2}
{:process :n3, :type :info, :f :ack-offset-to-primary, :value :n2}
{:process :c1, :type :invoke, :f :read, :value 5}]
Unable to linearize past this point!
({:process :c1, :type :ok, :f :read, :value 5})
lein test :only knossos.redis-test/redis-test
FAIL in (redis-test) (redis_test.clj:44)
expected: (not (empty? linears))
actual: (not (not true))
Ran 1 tests containing 38340 assertions.
6 failures, 0 errors.
Why the Last Read Broke Everything
Knossos found a system state that is possible under the Redis model we defined, but not linearizable with respect to the register model. The history stayed linearizable until that final read, but no ordering of operations can make it consistent.
The terminal state is the problem: n1 sits isolated with value 9 at offset 2, n2 is the primary with value 5 at offset 1, and n3 has nil at offset 0. Ignoring n3, which never participated, the sequence was:
- c2 writes
5to n1; n2 replicates and acknowledges the write. - n2 starts a no-op replication from n1.
- c2 writes
9to n1 while c1 concurrently reads it, seeing9. - n2 completes its no-op replication with no state change.
- A failover occurs: n2 becomes the new primary and n1 is isolated.
- n3 twice acknowledges its offset of
0to n2, both no-ops. - c1 reads from n2 and sees
5.
That last read is fatal. Before it, you could assume the write of 9 failed and the register was always 5, but c1's earlier successful read of 9 invalidates that. Alternatively, you could assume the final read of 5 failed, but it succeeded—leaving Knossos with no valid linearization.
Reads are a core part of linearizability, and Redis WAIT is not transactional. It lets clients read unreplicated state from the primary—a violation just as severe as reading stale data from a secondary. The conclusion is unavoidable: the proposed design is not only physically impossible but even generously optimistic formal versions of it are trivially non-linearizable.
That's the root of the FUD. You should doubt algorithms without proofs, distrust distributed systems without formal models, and worry that claims don't hold up. Now you have a concrete tool to test that doubt.
From Hand-Waving to Model Checking
Proving linearizability is harder than disproving it. Finding one counterexample, as done here, is far easier than showing every history is valid. The traditional approach is identifying all linearization points—the atomic moments where operations take effect—which is subtle and complex, especially when the point depends on runtime behavior or falls outside the code.
Proofs aren't for everyone, and they don't have to be. Model checking is a practical middle ground, letting ordinary programmers formalize algorithms and reason about them mechanically. Multiple tools exist for this:
- TLA+ (Leslie Lamport) is the canonical option for concurrency proofs but has a steep learning curve and difficult model composition.
- Spin (Bell Labs) is more programmer-friendly, modeling systems in Promela, with tooling that can even extract models from C code.
- Erigone is a reimplementation of Spin, and Line-Up covers C#.
- Knossos, built in Clojure, takes advantage of concise data-structure literals and immutable shared state to make modeling and checking linearizability easier—though it likely has bugs, so hand-check failures.
These systems all share a workflow: write the algorithm in an unambiguous form—modeling or programming language—and explore its state space to verify invariants. Some proof assistants can go further, proving the invariants hold always rather than just showing they can fail.
The toy system in this post has the key ingredients: state, transition functions, invariants, and a target model. Hierarchical data structures and functions break the model into manageable parts, with counterexamples generated from probabilistic paths through the state space.
Real-world models work the same way. The RAFT consensus model and proof sketch illustrate the definitions of state, transitions, and invariants, plus formal and English proof techniques. It's not a full, mechanically verified proof; it relies on unverified propositions like type safety. But it shows the kind of rigorous argument a database engineer should construct before claiming linearizability—one that catches obvious and subtle bugs before implementation, not after.
