Replication & consistency
Replication describes where copies live. Consistency describes which observations are legal.
Move a read through time
Drag a read across a write and see the model verdict change.
Loading activity… Enable JavaScript to interact; the course text remains readable.
Runs in your browser with synthetic state. This is not a live etcd cluster. Read the concept · Inspect real evidence
Learning goals
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.
One object, several contracts
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.
Replication does not choose the model
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.
Hands-on: compare two models
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.
Self-check
Is a successful search evidence that all executions of the service are correct?
No. It finds one legal explanation for this finite history. Other operations, schedules, objects and failures have not been checked.
Does a majority read always return the newest value?
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.
Read the originals
- Herlihy & Wing, 1990, the linearizability definition.
- MIT notes on consistency and linearizability, models and histories.
- etcd API guarantees, KV, watch and read-mode scope.
Study alongside MIT 6.5840
Lecture 8: Consistency and Linearizability · Lab 2: Key/Value Server
Compare real-time versus client-order constraints with an independent exhaustive oracle.
node tests/checker.test.mjsOur runnable exercise is an independent original, not the linked MIT assignment solution. Setup is on the reproduce page; no enrollment, grade or certification is implied.
Search the verified course map →