4.5Further Reading Regarding TSO

book p. 50 · ~5 min read

  • Collier's memory-copy model
  • processor consistency
  • write atomicity preview
  • TSO's formal lineage

Memory as per-core copies: Collier’s framework

Long before x86-TSO , Collier characterized alternative memory consistency models — including that of the IBM System/370 — with a deliberately abstract framework:

  • every core holds a full copy of memory;
  • a load reads its own core’s local copy; and
  • a store updates all the copies, subject to restrictions — and it is exactly those restrictions that define each model.

Were TSO defined this way, the restriction would read: a store writes its own core’s memory copy immediately, and then possibly later updates all the other memories — together. Notice how neatly that one sentence captures the chapter’s hardware story without mentioning hardware at all: “own copy immediately” is bypassing made model-level (a core always sees its own stores at once), and “the others later, together” is the buffered store finally entering memory order in a single instant.

TSO through Collier’s lensC1: S(x)=NEWC2C3C1’s memory copyx = NEWC2’s memory copyx = 0 → NEWat t₁C3’s memory copyx = 0 → NEWat t₁ — same instantimmediately (t₀)later — together (t₁)C1 reads NEW from t₀; everyone elseswitches from 0 to NEW in one instant.= bypassing + write atomicityProcessor consistency, in generalC1: S(x)=NEWC2C3C1’s memory copyx = NEWC2’s memory copyx = NEWat t₁C3’s memory copyx = 0, stillNEW only at t₂ > t₁immediately (t₀)t₁t₂ — later than C2Each core still sees C1’s stores in C1’s order,but C2 can see this store while C3 does not yet.TSO forbids the stagger; PC allows it

One store, S(x)=NEW from C1, in Collier’s per-core-memory-copy frame. Left — TSO: the local copy updates at once, every other copy in a single later instant. Right — general processor consistency: other copies update in order, but not necessarily together.

Processor consistency: TSO’s parent class

Goodman publicly discussed the idea of processor consistency (PC): a core’s stores reach the other cores in order, but do not necessarily reach them at the same “time” — as the right panel above shows, C2 may observe a store while C3 still holds the old value. (Gharachorloo et al. later defined PC more precisely.)

TSO and x86-TSO sit inside PC as the special case with two extra guarantees:

  1. each core sees its own store immediately (the bypassing behavior of §4.2’s Table 4.3); and
  2. when any other core sees a store, all other cores see it — no stagger.

The second property gets a name in the next chapter (§5.5): write atomicity. Keep the right panel in mind when you get there — chapter 5’s models relax exactly the guarantees that felt automatic here.

The formal lineage

To the best of the book’s knowledge, TSO was first formally defined by Sindhu et al. for SPARC. For x86 — which Intel and AMD have never formally pinned down themselves — the recommended formalization remains Sewell et al.’s x86-TSO from §4.3: an abstract machine and an equivalent axiomatic model that appear consistent with the vendor documentation and with current implementations.

Check yourself

1.In Collier's modeling framework — every core holds a full copy of memory, loads read the local copy — how would TSO be characterized?

2.Under processor consistency in general (not the TSO special case), core C1 performs one store S(x)=NEW. Can C2 observe x=NEW while C3 still reads x=0?

3.Which two extra guarantees turn general processor consistency into TSO?

4.Who first formally defined TSO, and what does the book recommend for reasoning precisely about x86?

4 questions