Replication describes where copies live. Consistency describes which observations are legal.
Compare linearizability, sequential consistency, causal consistency and eventual convergence; test a single-register history without confusing it with transaction isolation.
Prerequisites: causality and operation histories.
A register begins at 0. A writes 1 and receives success. Later B reads 0. If the read began after the write completed, linearizability forbids this history: every completed operation must fit one legal sequential execution respecting real-time precedence. An overlapping read could still return 0 by taking effect before the write.
A: write(1) ├──────┤ success B: read() ├────┤ → 0 Linearizable: impossible. Sequential: may order B before A.
Sequential consistency preserves each client's program order, but does not require cross-client real-time precedence. In the example, putting B's sole read before A's sole write can satisfy that weaker contract. Causal consistency preserves dependencies, including communicated observations; independent writes need not appear in one universal order. Eventual convergence promises replicas agree after updates stop and communication/reconciliation succeeds; it does not impose a per-read freshness deadline by itself.
These are contracts, not a ranking that selects the right answer for every application. A configuration change that must be visible to subsequent requests has different needs from a disconnected collaborative draft. You must also define conflict resolution, failure assumptions and the scope of an object.
Copying every write asynchronously can expose stale data. Asking a majority is not a complete linearizability algorithm either: ordering metadata, read protocols, write-back and membership rules matter. In this Lab etcd provides a concrete state-machine-replicated implementation, rather than a generic “R + W > N proves everything” argument.
etcd's default KV path provides a strong ordered contract. Its explicitly requested serializable read can read local state and may lag the quorum. Watch delivery has its own semantics and may be delayed. A watch notification stream should not be silently substituted for a fresh linearizable read.
Single-object linearizability and multi-object transaction isolation answer different questions. Two separately linearizable reads do not automatically form one transaction snapshot. An application read-modify-write needs an atomic compare/update or transaction if it must resist concurrent updates.
In the workbench, load “Stale.” Check linearizability, then sequential consistency. The same completed history fails the first and passes the second. Inspect the witness order, rather than treating a green label as sufficient explanation. Change the read to 9: no write produced 9, so neither model has a valid register execution.
The bounded search explores eligible operations, applying writes and accepting a read only when it equals the current integer state. It memoizes (chosen-operation set, register value). If it exhausts every legal order, it reports fail. If it runs out of budget, it reports inconclusive. This is a check of an input history under a tiny model, not a proof that etcd or another implementation is correct.
No. It finds one legal explanation for this finite history. Other operations, schedules, objects and failures have not been checked.
Not without a complete protocol. A quorum intersection is a building block. It does not alone define versions, resolve concurrent writes, or protect against stale leadership.