That depends on which event you mean. An instruction can enter a local store buffer before the store joins the shared memory order. This lesson uses abstract SC and FIFO-buffer TSO for ordinary aligned memory operations only, with X=Y=0 initially and no caches holding either line. It does not model device memory or every instruction in an ISA.
Operation | SC exercise | TSO exercise |
|---|---|---|
Store | Update shared memory when that operation takes its place in the total order. | Append to the issuing core's FIFO; a separate drain updates shared memory. |
Load | Read the latest preceding shared-memory write in the SC order. | Forward from the newest own matching buffered store, otherwise read shared memory. |
Program order | Every operation follows the preceding operation of its core globally. | Core issue stays ordered, but a different-address load can precede visibility of an older store. |
Prediction A: C0 issues W(X)=1 then R(X), starting X=0. With no other writer to X, both SC and this TSO model require the load to return 1. TSO obtains it through same-address forwarding if necessary. Prediction B: the SB test from the previous lesson can return 0,0 under TSO, because each load addresses the other location, not its own buffered one.
The store buffer's FIFO order also matters for message passing. With X=Y=0 initially, C0 issues W(X)=1 then W(Y)=1, while C1 issues r1=R(Y) then r2=R(X). In this SC and TSO subset, r1=1,r2=0 is forbidden: observing the Y store implies the earlier X store has become visible, and the reader's loads remain ordered. A model allowing different reorderings needs a separate analysis.
The Owens, Sarkar and Sewell x86-TSO report formalizes an operational write-buffer model. Our enumerator covers a small ordinary-load/store subset, not the complete report or an arbitrary processor implementation.
Not in this operational subset. It must forward the latest matching own buffered value. Bypassing a different address is the Store-to-Load relaxation used by SB, not permission to ignore an older same-address store.