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.
Cat model
Specified in cat cat file identified
An instance of the Herding cats generic framework (ppo additionally drops W->W); run here as litmus/models/abstract-pso.cat. Alglave et al. 2014
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
- Jade Alglave, Luc Maranget, Michael Tautschnig. Herding Cats: Modelling, Simulation, Testing, and Data Mining for Weak Memory. ACM TOPLAS, 2014. doi:10.1145/2627752