In single-threaded software execution, memory consistency is transparent: a read operation returns the value written by the most recent write. In a distributed environment where state is concurrently replicated across disparate nodes separated by variable network latencies, the phrase “the most recent write” loses physical meaning. Defining the semantic contracts governing concurrent reads and writes is the domain of Consistency Models. At the pinnacle of single-object consistency stands Linearizability (Herlihy and Wing, 1990)—the mathematical gold standard for making a distributed, multi-node cluster appear to external clients as though it were executing atomically on a single, instantaneous memory register.
1. Formalizing Execution Histories & Operations
To mathematically reason about consistency, an execution is represented as a history $mathcal{H}$ of events. Each client interaction with an object consists of an invocation event $ ext{inv}(op)$ and a matching response event $ ext{res}(op)$:
$$op = langle ext{inv}(op), ext{res}(op), ext{client}, ext{object}, ext{inputs}, ext{outputs}
angle$$
The operation spans a non-zero real-time interval $[t_{ ext{inv}}(op), t_{ ext{res}}(op)]$. We define a partial real-time precedence order $prec_{mathcal{H}}$ over operations:
$$op_1 prec_{mathcal{H}} op_2 iff t_{ ext{res}}(op_1) < t_{ ext{inv}}(op_2)$$
That is, $op_1$ strictly precedes $op_2$ in real time if its response occurred before $op_2$ was invoked by any client anywhere in the universe.
2. Linearizability (Atomic Consistency)
A concurrent execution history $mathcal{H}$ is defined as Linearizable if there exists a valid, equivalent sequential history $mathcal{S}$ satisfying three formal conditions:
- Sequential Equivalence: $mathcal{S}$ contains the exact same operations and arguments as $mathcal{H}$, with operations occurring sequentially (each invocation followed immediately by its response).
- Object Semantic Validity: $mathcal{S}$ obeys the sequential specification of the object (e.g. read returns the argument of the most immediately preceding write in $mathcal{S}$).
- Real-Time Precedence Preservation: For all operations $op_1, op_2 in mathcal{H}$:
$$op_1 prec_{mathcal{H}} op_2 implies op_1 <_{mathcal{S}} op_2$$
The Linearization Point
Linearizability implies that each operation takes effect instantaneously at a discrete mathematical moment $ au(op)$—its Linearization Point—situated strictly within its invocation and response window:
$$ au(op) in [t_{ ext{inv}}(op), t_{ ext{res}}(op)]$$
A crucial mathematical property of linearizability is composability (locality): if every individual object in a distributed system is linearizable, then the entire multi-object system is linearizable.
3. Sequential Consistency vs. Linearizability
Introduced by Leslie Lamport in 1979 for multiprocessor architectures, Sequential Consistency relaxes real-time ordering. An execution history is sequentially consistent if there exists a sequential history $mathcal{S}$ that preserves the program order of each individual process:
$$orall p, quad op_1 prec_p op_2 implies op_1 <_{mathcal{S}} op_2$$
However, sequential consistency does not preserve global real-time ordering across distinct processes. If process $A$ completes a write, waits 10 minutes, and phones an engineer running process $B$, sequential consistency allows process $B$ to read the old value indefinitely—as long as all nodes agree on the same logical sequence of events. Unlike linearizability, sequential consistency is non-composable.
4. The Spectrum of Weaker Consistency Models
Between linearizability and eventual consistency lies a hierarchy of consistency guarantees:
Strict Serializability (External Consistency)
While linearizability applies to single-object operations, Serializability applies to multi-operation ACID transactions (ensuring concurrent execution is equivalent to some serial order). Strict Serializability (or External Consistency) is the ultimate convergence: transactions are both serializable and linearizable—if transaction $T_1$ commits before transaction $T_2$ begins in real time, $T_1$ must be ordered before $T_2$.
Causal Consistency
By the CAP and PACELC theorems, linearizability requires sacrificing availability under network partitions. Causal Consistency is mathematically proven (Mahajan et al., 2011) to be the strongest consistency model achievable in a completely available system under network partitions. It enforces Lamport’s happens-before relation:
$$op_1 o op_2 implies op_1 <_{mathcal{S}} op_2$$
Concurrent operations with no causal connection ($op_1 parallel op_2$) may be observed in different orders by different nodes.
Session Consistency Guarantees
For client-centric architectures, distributed systems provide four standard session guarantees:
- Read-Your-Writes: A client’s successive reads always observe the effects of its own prior writes.
- Monotonic Reads: If a client observes state version $v_1$, it will never subsequently observe an older version $v_0 < v_1$.
- Monotonic Writes: A client’s writes are serialized in the order they were submitted.
- Writes-Follow-Reads: If a client reads version $v$ and submits write $w$, $w$ is causally ordered after $v$ globally.
