Coherence: for each single location, all writes fall in one order that every core agrees on (SWMR plus the data-value invariant). That single order of all writes to X is X's modification order. Consistency: which combinations of values across different locations a program may observe.
Yes. Extend the course model with Y in a separate line. Initially X=0 and Y=0 in memory and both caches are invalid for both lines. Consider abstract aligned ordinary-memory stores and loads. C0 issues store X=1 then load Y into r1; C1 issues store Y=1 then load X into r2. No fence or synchronization is present.
Core | Program order |
|---|---|
C0 | W(X)=1, then r1=R(Y) |
C1 | W(Y)=1, then r2=R(X) |
Under sequential consistency, SC, all four operations must fit one total order that preserves each core's program order. Two relations describe a candidate execution. Reads-from links a load to the store whose value it returned. From-read links a load to a store that comes after the store it read from, in that location's modification order: a load that returned the initial 0 of Y is from-read ordered before W(Y)=1. The candidate r1=0,r2=0 needs both loads to be from-read ordered before the other core's store. With the program-order edges, those requirements form a cycle, so this outcome is forbidden under SC with these initial values and no other writes.
In the FIFO store-buffer model of TSO used here, each core can issue its store into a local buffer, then load a different address before that store becomes globally visible. Both loads can therefore return 0 while each buffer still holds its own store. Later drains make X and Y equal to 1. Each location still has a coherent write history: initialised 0 followed by its single store of 1.
Contract, with X=Y=0 initially | Candidate r1=0,r2=0 | Reason |
|---|---|---|
SC | Forbidden | The global order must preserve both store-to-load program-order edges. |
Our TSO operational subset | Allowed | Loads of other addresses can execute before older buffered stores drain. |
Per-location coherence alone | Not sufficient to reject it | Each location can order the zero read before its store of 1. |
These are architectural executions, not a request/grant transaction. Do not infer cache states from the table: an issued store buffered ahead of the coherent cache controller is not already a completed coherent write. The SB/MP enumerator makes that distinction executable.
No. SWMR constrains simultaneous permissions per line. It does not establish SC's total order preserving all the programs' operations across the two lines.