Lamport and Sequential Consistency: Defining What Parallel Memory Should Mean
Leslie Lamport's 1979 definition of sequential consistency gave shared-memory programmers a precise contract: concurrent execution should look like one interleaving that preserves each processor's program order.
Multiprocessors made memory ordering a correctness problem
A sequential program can often be understood as if its instructions execute in source order, even when a processor internally pipelines, caches, or reorders operations. Multiprocessors make that illusion harder to preserve because one processor can observe another processor’s memory effects. Leslie Lamport’s 1979 paper began from exactly this concern: individually correct processors are not sufficient if their shared-memory interactions admit results that no sensible global execution explains.[1] The paper’s enduring contribution was a compact definition of the behavior programmers naturally expected.
The problem was not cache coherence alone
Coherence can ensure that processors eventually agree about values for one location while still allowing surprising orderings across multiple locations. A memory model must describe the larger ordering contract.
Sequential consistency defined execution as one legal global interleaving
Lamport wrote that an execution is sequentially consistent if its result is the same as if the operations of all processors occurred in some sequential order, with each processor’s operations appearing in that order according to its own program.[1] The definition is powerful because it does not prescribe one physical execution schedule. Many interleavings are legal. What matters is that there exists a single total order that explains the observed results while respecting local program order.
The definition separated programmer reasoning from machine implementation
Sequential consistency became useful because it is an abstract behavioral promise rather than a microarchitectural recipe. A machine can use caches, speculation, out-of-order execution, and other optimizations if their externally visible effects remain compatible with a legal sequentially consistent history. This separation resembles other successful abstractions in computing: programmers reason against a contract while implementers remain free to innovate beneath it.
A memory model is a set of allowed executions
The model does not say exactly how hardware must run. It says which outcomes must be impossible, providing a target that processors, compilers, runtimes, and programmers can reason about.
Sequential consistency proved intuitive but expensive to preserve universally
As multiprocessors became faster, designers found that strict global ordering can inhibit optimizations such as write buffering and aggressive memory pipelines. Sarita Adve and Kourosh Gharachorloo’s tutorial describes sequential consistency as the most intuitive shared-memory model while explaining why many systems adopted relaxed models to gain performance.[2] The resulting tradeoff became central to computer architecture: stronger models simplify reasoning, while weaker models permit more reordering and can make hardware easier to optimize.
x86 demonstrated that even familiar processors are not literally sequentially consistent
Peter Sewell and collaborators formalized the x86-TSO model and used classic examples to show executions that modern x86 processors can permit even though no sequentially consistent interleaving produces them.[3] Store buffers are a key reason. A processor may continue after issuing a store before that store is visible to another processor, allowing both sides of a two-thread test to read old values. x86 remains relatively strong compared with many architectures, but “relatively strong” is not identical to Lamport’s model.
Relaxation is observable only through concurrency
Many reorderings are invisible to single-threaded code. They become architecturally meaningful when another thread can observe memory between operations.
Programming languages eventually needed memory models of their own
Hardware is only one source of reordering. Compilers can move, combine, or eliminate accesses when language rules permit it. C++11 therefore introduced a formal concurrency model with atomic operations and multiple memory-order choices. Work by Mark Batty and collaborators helped formalize the emerging C++ model and connect it to hardware behaviors such as x86-TSO.[4] The language had to define not just what a processor may do but what transformations a compiler may perform while preserving concurrent meaning.
Sequential consistency survived inside weaker systems as a deliberately strong option
Modern concurrency APIs often expose sequentially consistent atomic operations as the easiest ordering mode to reason about. LLVM’s atomic guide explains that its sequentially consistent ordering provides acquire/release properties plus a total order across all sequentially consistent operations.[5] This is not identical to saying the entire program behaves under Lamport’s original model, especially when weaker atomics or data races are present. But it shows how Lamport’s concept became a named point in the design space rather than disappearing when relaxed memory arrived.
Strong ordering became something programmers can request selectively
Instead of imposing one global memory model on every access, modern systems often let programmers pay stronger ordering costs only where synchronization requires them.
Why sequential consistency belongs in the history of parallel computing
Sequential consistency matters because Lamport supplied a vocabulary for a problem that hardware trends made unavoidable. Once caches, compiler transformations, and weakly ordered processors entered mainstream systems, developers needed to distinguish physical execution order from the abstract order on which correctness proofs depend.[1][2]
The concept also became a reference point for every relaxed model that followed. Architects explain what their machines permit by comparing those behaviors with sequential consistency; language designers define stronger and weaker atomic orders against similar intuitions; verification tools ask whether executions violate the contracts programmers intended.
Lamport’s two-page paper therefore had influence far beyond its length. It did not solve memory ordering by insisting every machine behave sequentially. It made the tradeoff precise enough that later systems could weaken the model deliberately instead of doing so accidentally.
Works Cited
- 01
- 02
- 03
- 04
- 05
CodeHistory is a living archive. Citations document the evidence used for this edition; later evidence may refine the account.
Submit a research lead