The previous transactions preserve permission and data per location. This section asks which combinations of observations across operations an architecture permits. Work from a named model and explicit initial values, then connect ordering, atomicity and recovery to the coherent implementation.
Lesson | After it you can... |
|---|---|
Explain why SB 0,0 distinguishes SC from the stated TSO subset. | |
Separate issue, forwarding and global store visibility. | |
Enumerate exact outcomes with a bounded operational model. | |
Demand the published model and exact instruction test. | |
Distinguish ordering from memory cleaning. | |
Identify which store the acquire must read from. | |
Separate indivisibility from individual coherent accesses. | |
Name the endpoint behind a completion claim. | |
Separate execution from architectural observation. | |
Preserve protocol work during a selected replay policy. | |
Distinguish reservations, permission and value equality. | |
Build model-specific evidence before proposing a fix. |
Suggested order: memory models, synchronization, then speculation. The litmus examples add a second location Y in a different line, with X = Y = 0 initially unless stated otherwise. Protocol traces keep the shared model's cache and home notation.
Scope for the whole section: the examples are abstract hardware operations (loads, stores, fences and atomics on ordinary coherent memory), not C/C++ programs, whose compilers and language rules add their own reorderings. The litmus enumerator models SC and TSO only. Arm and RISC-V outcomes come from their published models, never from the enumerator.
SWMR checks permissions per line. The named SC program orders the payload write before the flag write and the flag read before the payload read. That cross-location contract is additional.