3.4Basic Idea of Sequential Consistency (SC)

Lamport’s two definitions

Arguably the most intuitive memory model is sequential consistency sequential consistency (sc) The result of any execution equals some total order (memory order) of all cores' loads and stores in which each core's operations appear in its program order (Lamport). defined in Chapter 3 — open in glossary , first formalized by Lamport. He built it in two steps. A single core is sequential if:

“the result of an execution is the same as if the operations had been executed in the order specified by the program.”

A multiprocessor is sequentially consistent if:

“the result of any execution is the same as if the operations of all processors (cores) were executed in some sequential order, and the operations of each individual processor (core) appear in this sequence in the order specified by its program.”

That total order of operations is the memory order memory order The total order (<m) on all cores' memory operations that an execution appears to perform. defined in Chapter 3 — open in glossary , written <m (op1 <m op2 means op1 precedes op2 in memory order). Each core’s program order program order The per-core total order (<p) of a core's memory operations as specified by its program. defined in Chapter 3 — open in glossary is written <p. Under SC, memory order respects each core’s program order: op1 <p op2 implies op1 <m op2. Other models will permit memory orders that don’t always respect program order — that is exactly what “relaxed” will mean.

Seeing an SC execution

Here is the flag/data program from §3.1 executing under SC (the book’s Figure 3.2). Each operation occupies one slot of the central memory order; the comment gives the value stored or loaded:

Under SC, every execution of this program ends with r2 = NEW. The only non-determinism — how many times L1 loads 0 before it finally loads SET — is unimportant. If in §3.1 you felt r2 must be NEW, you were independently inventing SC, just less precisely than Lamport.

The four (plus one) executions of Dekker

The value of SC shows even more clearly on Table 3.3’s program. Three outcomes are intuitive, and each corresponds to SC executions — six in total (outcome (NEW, NEW) alone has four interleavings; one is shown):

For outcome (0, 0), program order dictates S1 <p L1 and S2 <p L2, while the loaded zeros dictate L1 <m S2 and L2 <m S1. Chase the arrows: S1 → L1 → S2 → L2 → S1. Honoring all four constraints requires a cycle — which no total order can contain. The red arcs in panel (d) close that cycle visually.

What this means for builders

We have seen six SC executions and one non-SC execution. An SC implementation must allow one or more of the six and can never allow the seventh. (It need not allow all six — recall the partition view.) How to build such implementations, from naive to aggressive, is the business of the next four sections.