Distributed consensus, replication, and fault tolerance / personal lessonsLesson 4 of 17
Distributed systems · Lesson 4

What consistency promises to a client

Test linearizability, sequential order, causal order, and eventual convergence.

By the end: Find or refute a legal ordering of a small client history.

Specify the object before checking it

A read/write register stores one value. A write replaces it; a read returns the current value. A history records invocation and response events, including returned values. Linearizability asks whether each completed operation can be placed at one instant between its invocation and response so that the object’s rules hold. If one operation finishes before another begins, that real-time order must be preserved.

A read that begins after write(1) succeeds must return 1 if no intervening write exists. A read overlapping the write may return the old or new value, provided the whole history has a legal order. “Latest” is therefore not a rule that every overlapping read must see every in-flight write. A timed-out request might still take effect; incomplete histories need careful treatment beyond the complete histories in this small checker.

Construct a legal history one operation at a time

A register specification describes a sequence without mentioning replicas. Start with value 0. A write of 6 changes the value to 6, and every read before the next write must return 6. To check a concurrent execution, first retain each operation's invocation, response, argument, and result. Then ask whether some sequential arrangement obeys both that specification and the precedence constraints. The task is to find one legal explanation, not to guess which processor instruction actually changed a particular replica. An implementation may have a concrete event that provides this explanation, but the client contract concerns observable operations.

Consider this separate paper example. Write 6 runs from time 1 to time 6. Read A runs from time 2 to time 3 and returns 0. Read B runs from time 4 to time 5 and returns 6. Read A finishes before Read B begins, so A must precede B. Both reads overlap the write. Place A first, then the write, then B. At A the register still contains 0; the write changes it to 6; B now sees 6. You can place the write's imagined instantaneous effect between times 3 and 4, inside its invocation interval. All results have one legal explanation even though the write responds after both reads.

Now reverse only the read results. A returns 6 and B returns 0, with the same intervals and no other write. A's result forces Write 6 before A in any legal sequential arrangement. Real-time precedence forces A before B. Those two requirements put Write 6 before B, so B must return 6. No placement of the write inside its interval repairs the contradiction. Overlap lets an operation take either position when the other constraints allow it. It does not give each read an independent choice of old or new value. The entire history must use one consistent order.

This method separates necessary constraints from optional choices. Draw a precedence edge whenever one response occurs before another invocation. Do not add an edge merely because one invocation occurs earlier. For a read returning a noninitial value, locate a write that could supply it. Place that write before the read, then check whether another intervening write would replace its value. A proposed explanation fails if it requires an operation before one of its mandatory predecessors or makes a read return a value different from the current register state.

The time numbers in these examples describe an ideal shared history for reasoning. They are not a requirement that production clients have perfectly synchronized clocks. Collecting reliable invocation and response evidence across machines is a separate measurement problem. A single observer can establish some precedence relationships without knowing absolute time, for example by receiving one response and only then sending another request. Uncertain clock offsets can leave other relationships unresolved. A checker cannot recover missing evidence merely by sorting local timestamps. The model below assumes that the supplied intervals already describe the intended order accurately.

Weaker contracts preserve different orders

Sequential consistency requires a legal single order preserving each client’s program order, but does not require the real-time precedence between different clients that linearizability requires. Causal consistency preserves dependencies such as an answer following a question; unrelated concurrent operations may appear in different orders to different readers. These are different contracts, not percentages of correctness.

Read-your-writes is a session guarantee that prevents a client from losing sight of its own successful updates. Monotonic reads prevent a session from moving backward through observed versions under an appropriate version order. Neither guarantee alone gives every client a globally current view. Eventual consistency generally promises convergence once updates stop and required communication and repair continue. Without additional bounds it does not promise convergence within five seconds or preservation of an application invariant during disagreement.

Distinguish a shared sequence from a session guarantee

The weaker contracts in the preceding section discard different constraints. Use another paper case to isolate one difference. Ada completes Write 8 and later tells Bo, outside the register interface, to issue Read B. Bo reads 0. With only those two register operations, a sequentially consistent explanation can put Bo's read before Ada's write. It preserves each client's program order because each client performed just one operation. Linearizability forbids that explanation because the write finished before the read began. Sequential consistency does not mean each client always gets the latest completed update from other clients.

The scope of the recorded history matters here. If the service also promises causal consistency and tracks the dependency conveyed by Ada's message, Bo's read may carry an obligation to include Ada's write. A causal implementation needs a way to transmit and honor that dependency. It cannot infer every conversation that occurs outside its interface. A system description should say whether a session token, version metadata, or some other mechanism conveys the dependency. Calling a database causally consistent does not make an unrecorded telephone conversation visible to its replicas.

Read-your-writes addresses a different case. Ada changes her profile, receives success, and refreshes it through another server. A session mechanism can require the second server to catch up to Ada's observed version or route the refresh to a suitable replica. That server may still lack unrelated updates from Bo. Monotonic reads can similarly prevent Ada from observing version 10 and then version 7 when she switches replicas. These statements assume a meaningful version order for the object. With concurrent branches, deciding whether a version includes earlier observations may need causal metadata rather than one timestamp.

Eventual convergence says less about the interval before replicas reconcile. Suppose two replicas accept different profile descriptions while disconnected. A documented merge rule might select one description when communication resumes. If updates stop and the repair mechanism eventually exchanges the necessary information, both replicas can reach the same result. This promises neither that the selected text represents the user's intention nor that every acknowledged version survives as the final value. A last-writer rule also needs a defined ordering of versions. A larger wall-clock timestamp need not identify the operation that occurred later in real time when clocks disagree.

Before the model, separate these questions on paper. Does the contract require one shared operation order, preservation of particular dependencies, or only a later equal state? Which obligations continue when a client changes servers? What communication and failure assumptions support eventual progress? A follower that waits indefinitely for a missing version may avoid a stale response but fail to provide useful liveness. A replica that immediately returns its local value may preserve a weaker contract while violating a stronger one. Neither behavior has a meaningful correctness verdict until the promised contract and its progress conditions are stated.

Work through the model

Can these operations appear atomic?

Time increases to the right; register starts at 0Write 1Read → 1Intervals may overlap without prescribing their logical order.

Allowed order: W1, R1.

Each line runs from invocation to response on an ideal shared timeline. The checker enumerates orders of this tiny complete history. It is not a verifier for a database implementation. Choosing a preset replaces the history.
ContractRequired orderingWhat it does not alone promise
Linearizable registerReal-time precedence plus register rulesAtomic transactions across multiple keys
Causal consistencyDependencies before their consequencesOne order for all concurrent writes
Eventual convergenceAgreement after updates stop and repair succeedsA maximum staleness bound
Contracts specify legal observations, not implementation brand names.

Read a witness as an explanation rather than a measurement

The history control presents three fixed complete histories. It does not accept arbitrary database traces. In Read after success, the write finishes at time 3 and the read starts at time 4. The checker must place the write first, then verify that the read returns 1. In Stale read after success, the intervals impose the same order but the read returns 0. The specification rejects that result. In Read overlaps write, a read returning 0 fits before the write, even though the write was invoked first. Choosing a preset replaces the whole history rather than sending messages to a simulated cluster.

The checker searches candidate orders by maintaining a current register value, initially 0. It may choose an operation next only when no remaining operation must precede it in real time. A write updates the current value. A read is eligible only when its recorded result equals that value. If a branch gets stuck, the search tries another eligible order. Reaching the end supplies the displayed witness. This is an exhaustive search for the bounded input, not a probabilistic judgment that an execution looks plausible. The underlying model limits histories to eight distinct complete operations.

A witness states that at least one permitted sequential explanation exists. Several explanations may exist when operations overlap. The first one found is not evidence that the system internally used that order. Conversely, failure to find a witness refutes linearizability for this supplied complete register history, assuming its intervals and results are accurate. It does not diagnose whether the cause was stale routing, an application bug, a bad trace, or a failed replication rule. Those explanations need observations from the implementation. The control deliberately isolates specification checking from protocol diagnosis.

For guided exploration, predict each preset's answer before selecting it, then identify the exact precedence relationship responsible. On paper, extend the overlapping preset with a second read that starts after the first read finishes but still before the write responds. Give the first read result 1 and the second result 0. Try every possible position for the write relative to those reads. The earlier read requires the write before it, while the later read requires the write after it. Their nonoverlap makes those requirements incompatible. This extension is a reasoning case, not an extra preset or an editable feature of the control.

Incomplete operations require a different treatment. If a write times out without a recorded response, it may still have taken effect. A linearizability analysis can sometimes complete such an operation with an imagined response and include it, or omit an operation that never took effect, subject to the formal history rules. Simply deleting every timed-out write can turn a legal read into an apparent unexplained value. Simply counting every invocation as a completed write can impose effects that never occurred. The displayed checker avoids this issue by handling complete operations only. Its bounded result does not certify a storage system under arbitrary failures.

Consistency is not transaction isolation

Linearizability is usually discussed for individual objects or operations. Serializability says transactions have effects equivalent to some serial transaction execution. Strict serializability also respects real-time order. A collection of linearizable single-key reads and writes does not automatically make a multi-step transaction serializable. Another transaction can intervene between the steps.

To read an expert’s claim, ask which operations and objects it covers, which histories are allowed, and what happens during a failure. “Strong consistency” without an operational definition leaves these questions unanswered. For a seat reservation, an atomic conditional update on the authoritative seat may suffice. Reading a stale display cache can be acceptable if the final purchase rechecks availability and the interface does not promise ownership prematurely.

State the boundary of an atomic operation

An operation's boundary determines what the consistency promise protects. A service can provide a linearizable Increment operation on a counter. It can also provide separate linearizable Read and Write operations without making a client-side increment safe. Suppose the counter begins at 10. Ada reads 10, Bo reads 10, Ada writes 11, and Bo writes 11. Every operation has a legal position, but the final value records only one increase. The missing guarantee concerns the combined read and modification. An atomic increment chooses one position for the whole state transition, so two successful increments would produce 12 under the stated counter rules.

A conditional operation can combine observation with a decision. Compare-and-set means replacing a value only if it still equals an expected value, with that test and replacement occurring atomically. If Ada and Bo each try to change revision 4 to their own revision 5, only one may succeed when both compare against the same current revision. A rejected attempt must read the new state and reconsider its work. A revision number can help distinguish separate occurrences of an equal-looking value. If the value changes from empty to occupied and back to empty, checking only the word empty does not prove that no intervening operation occurred.

Transactions extend the reasoning to a chosen group of actions. Consider two accounts, each with balance 50, and a transfer of 10. The transfer should change the balances to 40 and 60 together. Individually atomic writes can expose 40 and 50 between those changes. A transaction with an appropriate isolation contract prevents observers covered by that contract from treating the partial change as a completed transfer. Serializability asks for a legal serial order of transactions; strict serializability also constrains that order by real-time precedence. Later lessons examine transaction commit separately because deciding whether a transaction commits does not itself settle its isolation rules.

Even a linearizable read is not a reservation of future state. If a read reports that one ticket remains, another operation may claim it before the reader sends a purchase request. The read can have been entirely correct at its position in the history. To promise ownership, the service needs an atomic transition that checks and assigns the ticket, and it must base the purchase response on that transition's result. A display can tolerate stale information while the final ownership operation remains strict, provided the interface does not describe the displayed availability as an already granted claim.

When reviewing a service specification, write the operation signature in words and name its success result. Is purchase one indivisible request or a sequence assembled by the browser? Does a successful response promise a durable reservation or only acceptance for later processing? Are reads single-object operations or a consistent view across several objects? These choices decide which histories are forbidden. The replication lesson next explains how stored entries, commitment, and application can support a response contract. It does not make a poorly chosen operation boundary atomic merely by copying its individual steps to several machines.

Exercises

An overlapping read

Write(1) runs from time 1 to 5. Read returns 0 and runs from time 2 to 4. Initial value is 0. Is this necessarily a violation?

Hint

Can the read be ordered before the write inside their intervals?

Worked answer
HistoryLegal order
Read overlaps writeRead 0, then write 1
Read starts after write successWrite 1, then read must return 1
Real-time constraints come from completed-before-invoked relationships.

No. Place the read before the write while both are in flight. The returned 0 is then legal. If the read instead began after the write’s successful response and no other write occurred, returning 0 would violate linearizability.

Two reads and a reservation

Every single-key read and write is linearizable. Two clients both read seat=empty and then both write their own names. Have you prevented two successful reservations?

Hint

There are four operations, not one conditional transition.

Worked answer
OrderOperationResult
1Ada readsEmpty
2Bo readsEmpty
3Ada writesAda
4Bo writesBo
Each operation can be linearizable while the application protocol is wrong.

No. A legal order is read empty, read empty, write Ada, write Bo. Use an atomic compare-and-set or transaction that combines the check and assignment, and define success from that atomic result. Linearizable components do not join separate operations into one atomic action.

Sources and further reading

The explanations and worked answers above stand alone. These references provide the original algorithms, assumptions, and deeper proofs; they are not required downloads.