3.5A Little SC Formalism

The notation

To compare SC with the weaker models of the next two chapters, we need it in a form we can manipulate. The book adopts the axiomatic formalism of Weaver and Germond (the SPARC manual — chapter 11 discusses axiomatic specification as a method):

• $L(a)$ and $S(a)$ — a load and a store to address $a$;
• $<_p$ — 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 : a per-core total order capturing the sequence in which that core logically executes memory operations;
• $<_m$ — 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 : a total order on the memory operations of all cores.

SC in two rules

An SC execution requires:

(1) Program order is preserved — all cores insert their loads and stores into $<_m$ respecting their program order, regardless of whether the addresses are the same or different ($a = b$ or $a \neq b$). Four cases:

(2) The value rule — every load gets its value from the last store before it in memory order to the same address:

where $\operatorname{MAX}_{<_m}$ denotes “latest in memory order.”

Atomic read-modify-write read-modify-write (rmw) An atomic instruction (e.g., test-and-set, fetch-and-increment, compare-and-swap) whose load and store appear consecutively in memory order. defined in Chapter 3 — open in glossary instructions (details in §3.9) add one more constraint: each RMW’s load and store must appear consecutively in $<_m$ — no other memory operation, to any address, may interpose between the test and the set.

The ordering table

The book compresses rule (1) into a table — the template every later model will relax. An “X” means the program ordering (Operation 1 before Operation 2) is enforced:

Keep this table in mind as a baseline. In Chapter 4, TSO will erase exactly one X (Store→Load — the write-buffer relaxation you saw break Dekker in §3.1); Chapter 5’s relaxed models will erase nearly all of them and hand you a FENCE instruction to paint Xs back where you need them.

Safety and liveness

“An SC implementation permits only SC executions” — strictly speaking, that is the safety property (do no harm). Implementations also need liveness (do some good): a store must eventually become visible to a load repeatedly attempting to read that location — eventual write-propagation eventual write-propagation Liveness property: a store eventually becomes visible to a load repeatedly attempting to read that location. defined in Chapter 3 — open in glossary , typically ensured by the coherence protocol. (Without it, a machine that never propagated anything would be vacuously “SC.”) Starvation avoidance and fairness also matter but lie beyond this discussion.