Distributed consistency — extended reference

This reference preserves the earlier detailed chapter and its citations. Start with the guided explanation, then use these sections for additional mechanisms and qualifications. References to the original lesson sequence are historical.

Part 5: Correctness across machines

Prerequisites: Lesson 25 and the preceding foundations.

Learning outcomes

• Distinguish linearizability, serializability, strict serializability, causal guarantees, and session guarantees.
• Explain CAP using a concrete partition and the theorem’s availability definition.
• Use PACELC as an architectural comparison while preserving workload and consistency assumptions.

Correctness is a set of permitted histories

A user updates a profile in one region, receives success, then reads the old profile in another. Whether this is a bug depends on the promised consistency contract. A catalog might permit bounded staleness. A transfer confirmation might require stronger ordering. The word consistent is too broad to resolve the question.

A history records operations, their invocation and response times, and returned values. A consistency model defines which histories are legal. This makes guarantees testable and prevents a product label from standing in for a precise contract.

Linearizability

For an object with a sequential specification, linearizability requires each completed operation to appear to take effect at one point between its invocation and response, while respecting the real-time order of nonoverlapping operations. If a write completes before a read begins, the read cannot be placed before that write in the object’s legal order.

An incomplete operation may have taken effect even without a response. That is why timeouts remain uncertain. Linearizability does not mean every caller sees an instantaneous physical update; communication still takes time. It constrains the histories the interface permits.

Scope matters. Linearizable operations on individual keys do not automatically provide one atomic transaction across several keys. A transfer needs a multi-object specification and transaction protocol. Strong single-key behavior is useful but does not establish all relational invariants.

Serializability and strict serializability

Serializability concerns transactions: the outcome must be equivalent to some sequential ordering of them under the relevant model. It does not by itself require that order to match every real-time relationship observed by clients.

Strict serializability adds real-time ordering for transactions. It combines atomic transactional behavior with an order respecting completed-before-started relationships. This is a stronger contract than a consistent snapshot alone.

A database can use parallel execution and still provide serializability through locking or validation. Conversely, serial execution within one component does not automatically establish a global strict-serializable contract if replicas serve stale reads or several components make independent decisions. Execution strategy and external guarantee must be analyzed separately.

Session and causal guarantees

Read-your-writes ensures a session can observe its completed writes under the defined scope. Monotonic reads prevent a session from moving backward to an older observed state. Monotonic writes and writes-follow-reads constrain other session relationships. These guarantees can improve user experience without requiring a single global real-time order for everything.

Causal consistency preserves causally related operations. If a reply depends on a message, a reader should not observe the reply without its causal prerequisite under the model. Concurrent independent operations may appear in different orders. Tracking dependencies can require metadata and retention.

Session identity must survive routing and reconnection if the guarantee is expected to survive them. A cookie or token may carry a version watermark, or the service may route the session to an appropriate replica. A guarantee implemented only by staying on one connection can disappear when a mobile client reconnects unless the contract says otherwise.

Eventual consistency and convergence

Eventual consistency generally requires replicas to converge under stated conditions such as no new updates and eventual successful communication. It does not specify how stale a read can be during ongoing activity or whether an intermediate conflict resolution matches the application’s intent.

A conflict policy is still required. Last-write-wins selects one version under a timestamp order but can discard a concurrent update. A mergeable data type can preserve selected concurrent operations if its algebra and implementation assumptions hold. A set, counter, and unique item owner require different semantics.

An illustrative replica lag of two seconds at 5,000 writes per second corresponds to about 10,000 unapplied writes if rate is steady. The count does not describe which keys are affected or whether the lag is bounded. A lag metric should be interpreted alongside operation and placement patterns.

CAP during a partition

The original Gilbert–Lynch CAP result concerns atomic, or linearizable, read/write storage and formal availability under a network partition in its stated model. Here C means linearizability, including the real-time constraint; it is not interchangeable with transaction serializability that omits real-time order. It is not a general menu where every product permanently chooses two letters and ignores the third.

Suppose two separated regions must both accept an exclusive claim on the same item. If they cannot communicate and each must return a successful decision without waiting, they cannot both ensure one globally authoritative owner for conflicting claims. A system can reject or delay one side, weaken the contract, or preallocate independent rights before the partition. Each choice changes behavior under a specific failure.

Formal availability is stronger than an uptime percentage: the model concerns responses to operations at nonfailed nodes under the stated conditions. Product discussions often use availability more loosely. The course keeps the formal result separate from operational SLOs and from marketing labels.

PACELC and normal-operation tradeoffs

PACELC highlights that even without a partition, a distributed system can trade latency against consistency depending on where coordination occurs. A remote synchronous acknowledgment can increase normal write latency. A nearby asynchronous read can reduce delay while exposing staleness.

This is a reasoning framework, not a complete classification of every modern database. Different operations and configurations in the same product can make different tradeoffs. A global read-only query, a tenant-local write, and a cross-region transaction should be described separately.

The useful question is where the required evidence for an answer resides. If a read needs proof that no newer authoritative write exists, it may need leadership, quorum, lease, or version information. Avoiding that communication requires either already valid evidence or a weaker promise. An implementation cannot eliminate a necessary fact merely by choosing a faster API.

Build concrete histories

Consider a register initially zero. Writer W completes write(1) before reader R invokes read(). A returned zero violates the ordinary linearizable register specification. If the read overlapped the write, either ordering may be legal depending on the full history.

Now consider a transfer transaction and a separate balance query. Per-key linearizability can still permit a query to read one account before the transfer and the other after if the query is not an atomic transaction. The result can mix states even though each individual key operation is valid. The required scope must therefore be explicit.

For causal behavior, imagine posting a reply only after reading an original message. A replica exposing the reply without the original violates that dependency under a causal contract, even if both eventually appear. This example differs from two independent posts whose relative order may remain unconstrained.

Testing and interpretation

A correctness checker needs an operation model, a recorded history, and the claimed guarantee. Missing invocation or response events can create ambiguity. Time measurements need enough accuracy to establish relevant nonoverlap, but a checker should not infer a strict order from unsynchronized machine timestamps without justification.

Passing a finite test does not prove an implementation correct for all executions. It provides evidence against specific failure patterns. Formal reasoning, model checking of bounded components, targeted faults, and production observation complement one another. The goal is a coherent guarantee supported by both design and evidence.

Work through a history with overlapping operations

Consider a register initially zero. Client A invokes write(1) at time 10 and receives success at time 30. Client B invokes read() at time 20 and receives zero at time 25. A linearizable interpretation can place B’s read before A’s write because the operations overlap. Physical response order alone does not force the write to precede the read.

Now change B’s invocation to time 35, after A’s success. Returning zero is no longer permitted by the simple linearizable register specification, assuming no intervening write. The completed-before-invoked relation constrains the legal order. This is stronger than saying every replica eventually receives one.

A write timing out at time 30 is different from receiving an explicit rejection. It remains pending from the observer’s perspective and may be included as completed in a legal extension of the history if it took effect. A later read returning one can therefore be legal even though A never received success. Correctness checkers and application retry logic both need this distinction.

time:       10      20      25      30      35
A write(1): [-----------------------]
B read():           [--0--]                 overlapping: legal
C read():                                   [--0--]  later: illegal

The diagram assumes A’s closing bracket means successful completion, C has no overlapping later write, and the register’s sequential specification is ordinary last-write behavior. Adding other operations can change the analysis, which is why complete histories matter.

Serializability can permit an older ordering

Suppose T1 writes X=1 and completes. Later T2, using a permitted stale transactional snapshot, reads X=0. If the system promises serializability without a real-time constraint, the history may be explained by serial order T2 then T1. That order contradicts observed elapsed time but can satisfy the abstract serial-equivalence requirement. A strict-serializable contract forbids this reversal when T1 completed before T2 began.

This example is about possible contracts, not a claim that every serializable database serves such reads. Implementations can provide stronger behavior than their minimal labels, and read-only transactions can have specialized modes. The correct comparison uses the documented operation and mode, including replica routing.

A transaction reading multiple keys also needs one atomic view under its contract. If X and Y start at zero, a transaction writes both to one, and a reader separately fetches X before and Y after, it can observe (0,1). Each individual fetch could be linearizable while the pair is not an atomic read transaction. Per-object guarantees do not automatically compose into arbitrary application transactions.

Linearizability is compositional across objects under its model, but that compositional property preserves the individual object specifications. It does not invent a new atomic operation spanning them. To demand an atomic transfer or multi-key snapshot, define that operation in the interface and supply a protocol that implements it.

Causality follows dependencies rather than physical simultaneity

Alice posts a message. Bob reads it and writes a reply. Carol reads Bob’s reply. A causal contract includes the dependency from original to reply: exposing the reply should not omit the prerequisite according to the relevant visibility model. Independent messages written without observing each other can remain concurrent and appear in different relative orders.

A causally consistent system needs dependency information or an equivalent placement/communication strategy. If a client moves between replicas, it can carry a context describing what it has observed. The destination replica may wait to catch up, fetch prerequisites, or route elsewhere. Causal behavior is not free local availability when required dependencies are missing.

Metadata size depends on how dependencies are represented. Per-object version vectors can grow with participants; compact tokens can summarize progress under an architecture’s assumptions. Tracking every user’s device forever is different from tracking a fixed replica group. Metadata design affects scalability and garbage collection as directly as the stored values do.

Causal consistency still permits concurrent conflicting actions. Two users can independently claim the same exclusive item unless an additional coordination or merge rule prevents it. Causal order preserves dependencies; it does not provide arbitrary uniqueness or inventory conservation. Matching a consistency model to an invariant requires asking what concurrent actions are allowed to mean.

Session guarantees can improve UX without global coordination

After changing a profile, a user expects to see the new value. Read-your-writes can provide that behavior while unrelated users read asynchronously replicated copies. A session token can carry the minimum version the user must observe. A read gateway sends the request to a replica at or beyond that version or waits according to a bounded policy.

Monotonic reads prevent the user from seeing version 12 and then version 10 merely because routing changed. The token must track a meaningful version order for the data being read. A single scalar watermark can work in some globally ordered systems; independently partitioned histories may need richer context.

A session guarantee is only as durable as its session identity. If it disappears on reconnect, a mobile user changing networks may observe older state unexpectedly. If the contract spans devices, the service needs a way to transfer or retain context. This becomes a product and authentication design issue rather than a storage-only setting.

Session freshness does not establish a global invariant. Two users can each read their own accepted write and still have concurrent conflicting claims resolved later. The guarantee improves one person’s continuity of observation. It should not be advertised as equivalent to strictly serializable transactions over all users’ actions.

Convergence needs a defined merge algebra

Suppose replicas independently increment a counter. A last-write-wins register can discard one increment if each writes a replacement value derived from zero. A mergeable counter records contributions so the replicas can combine them without losing increments under its assumptions. The data type determines which concurrent operations are preserved.

A grow-only set merges by union, which is associative, commutative, and idempotent. Deletion complicates the representation because an absent element might mean “never added” or “removed after an observed add.” Tombstones, unique operation tags, or causal context can preserve the distinction. Garbage collection must not let an old add resurrect a removed value when delayed state arrives.

These techniques do not directly solve exclusive ownership. Merging two claims by keeping both violates uniqueness; keeping one loses an accepted claim. Some applications can tolerate explicit conflict resolution, while others require coordination before success. The acceptable business semantics determine whether a coordination-free merge is suitable.

Convergence also assumes eventual communication and compatible merge rules. Permanent partitions or diverging software versions can prevent convergence. During ongoing writes, eventual consistency alone gives no fixed staleness bound. A product requiring “visible everywhere within two seconds” needs a stronger operational and failure contract than eventual convergence after updates stop.

A partition scenario with actual product consequences

Consider one remaining concert ticket and two disconnected regions. Both receive a purchase attempt. If each region must return success immediately using only its local copy, both can sell the ticket. To preserve one-owner semantics, the architecture can restrict selling authority to one side or preallocate disjoint rights before the partition. The side without authority returns failure or waits.

Preallocating inventory can improve regional availability when the resource is divisible. Region A gets sixty units and B forty; each sells within its allocation during disconnection. Moving unused rights later requires coordination, and a single indivisible ticket cannot be allocated to both simultaneously. Escrow changes where the invariant is enforced rather than removing it.

Returning a quick error may satisfy an operational response-time metric but does not make the service available in the formal CAP sense for an operation that must succeed according to its specification. A site can show excellent uptime while rejecting an important class of writes. Availability metrics should distinguish transport responsiveness from successful permitted operations.

After reconnection, asynchronous reconciliation cannot undo every real-world consequence. A refund may compensate financially but cannot make two customers both attend with the same exclusive seat. This is why consistency decisions must be tied to domain meaning, not only to database vocabulary.

Bounded staleness and bounded latency are different promises

A replica can report an applied position or a commit-time watermark, but interpreting staleness requires a defined reference. Time since the last received record is not enough during idle periods, and a wall-clock timestamp needs clock assumptions. A read may need a heartbeat or leader contact to prove it is within a requested bound.

If a bounded-staleness read cannot establish freshness before its deadline, it must wait, route elsewhere, reject, or relax the promise explicitly. Returning whatever is local quietly changes the contract. A fast stale response and a timely fresh response are different products even when their APIs share a method name.

For the earlier two-second lag at five thousand writes per second, ten thousand unapplied writes is a backlog estimate under a steady-rate assumption. It does not mean every key is two seconds old. A cold key may be current while a hot key has many missing updates. Freshness should be measured at the scope relevant to the request.

Translate guarantees into acceptance evidence

A history recorder needs stable operation identities, input/output values, invocation and completion events, and explicit uncertain outcomes. A checker then searches for a legal interpretation under the selected model. It must not impose cross-machine order solely from uncalibrated wall clocks. Per-process order and observed response-before-next-invocation relationships often provide stronger evidence.

Finite testing can find violations but cannot prove every execution safe. Protocol reasoning establishes invariants; model checking explores bounded state spaces; fault-injection histories challenge implementation details. Each addresses a different source of error. The curriculum’s scenario traces are explanatory specifications that help determine what those tools should check.

A precise service contract finally names the scope, freshness, transaction boundaries, failure behavior, and retry semantics. “Strong consistency” without these dimensions is too vague to guide either implementation or UX. Once the history is explicit, replication mechanisms can be evaluated according to the evidence they gather before returning an answer.

Use a contract matrix for the running scenarios

The matrix selects properties for explanation rather than prescribing universal product requirements. A profile used as an authorization record may need a stronger contract than a decorative biography. A dashboard used to authorize spending may need current transactional evidence. The same stored data can serve operations with different correctness needs.

A consistency label should be attached to the operation’s observable behavior, not only to a database cluster. One service may provide strictly ordered writes, session-fresh account reads, and deliberately stale catalog browsing. This can be a coherent architecture if callers know which path they are using and authoritative decisions do not depend on weaker observations accidentally.

Distinguish stronger evidence from faster answers

A local cache can answer in microseconds while lacking evidence of recent writes elsewhere. A quorum-confirmed path can gather stronger evidence while spending additional milliseconds. A lease can reuse evidence acquired earlier under a validity bound. These are different ways to satisfy or relax an observation contract; they are not simply different implementations of an identical always-current read.

When evaluating an optimization, state the history it excludes. A session watermark excludes reads older than the caller’s known write. A linearizable read excludes observations inconsistent with a single real-time-respecting object history. A transaction protocol excludes multi-key anomalies according to its isolation model. Precision about excluded histories makes both benefits and remaining risks concrete.

Design conclusion

Consistency is an interface contract over histories and scopes. State whether the guarantee concerns a key, a transaction, a session, a replica, or the entire service, and describe behavior during failures. Lesson 27 examines replication mechanisms that can implement different choices within this vocabulary.

Sources and further reading

• Herlihy and Wing: Linearizability, 1990
• Gilbert and Lynch: CAP, 2002
• Abadi: Consistency tradeoffs, 2012

Course index · Lesson plan