Partial Store Order PSO
Extends TSO by additionally allowing store-store reordering to different addresses. A thread's writes to distinct locations may become visible to other threads out of program order.
Properties
Property vector author-extrapolated — set only where the model’s definition pins the cell down (unknown cells are omitted); cells citing a specific source are marked.
- Reordering sound
- yes Store→Load
- yes Store→Store
- no Load→Load
- no Load→Store
- Reasoning guarantees
- yes Coherence
- yes No undefined behaviour
- yes In-order execution
- yes No out-of-thin-air
- Atomicity guarantees
- yes Multicopy atomic
Ordering relationships
- Strictly weaker than
- Total Store Order (TSO) — PSO additionally allows store-store reordering to different addresses.
- Strictly stronger than
- Relaxed Memory Order (RMO) — RMO allows all four reordering types including load-load and load-store.
- IBM POWER Memory Model — Empirically PSO is a subset of POWER: every PSO-allowed behaviour is also POWER-allowed, while POWER additionally allows load-load reordering (e.g. MP+sync+po) and non-MCA behaviour that PSO forbids. No PSO-allowed/POWER-forbidden witness exists on the standard litmus families, so the earlier 'incomparable' classification was too generous. See litmus/strictly-weaker/PSO-vs-POWER.
- Equivalent to
- Relaxed Memory Models: an Operational Approach (RMMOA) — RMMOA is an operational model whose out-of-order propagation of writes to different locations matches PSO's store→store relaxation.
References
- SPARC International. The SPARC Architecture Manual, Version 8. Prentice Hall, 1992. sparc.org/technical-documents/
- Jade Alglave. A Shared Memory Poetics. PhD Thesis, Université Paris 7, 2010. www.cl.cam.ac.uk/~pes20/weakmemory/thesis.pdf
- Sarita V. Adve, Kourosh Gharachorloo. Shared Memory Consistency Models: A Tutorial. IEEE Computer 29(12), 1996. doi:10.1109/2.546611