IBM POWER Memory Model
The POWER architecture model allows extensive reorderings and non-multi-copy-atomic (non-MCA) behaviour: a store can be visible to one thread before others. Requires explicit barriers (sync, lwsync, isync) or dependencies for ordering.
Ordering relationships
- Strictly weaker than
- Partial Store Order (PSO) — 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.
- Strictly stronger than
- Cache Coherence — POWER enforces coherence as a baseline.
- Compilation target of
- Intermediate Memory Model (IMM) — IMM compiles correctly to POWER.
- Linux Kernel Memory Model (LKMM) — Linux kernel primitives compile correctly to IBM POWER.
- Incomparable with
- ARM Memory Model — Over the common instruction set ARMv7 and POWER coincide on every standard litmus family (verified against herd7's arm.cat and ppc.cat). Their incomparability is instruction-level: POWER's lightweight cumulative barrier lwsync (which allows SB) has no ARMv7 counterpart. See litmus/incomparable/ARM-vs-POWER.
References
- Susmit Sarkar, Peter Sewell, Jade Alglave, Luc Maranget, Derek Williams. Understanding POWER Multiprocessors. PLDI 2011, 2011. doi:10.1145/1993498.1993520
- Sela Mador-Haim, Luc Maranget, Susmit Sarkar, Kayvan Memarian, Jade Alglave, Scott Owens, Rajeev Alur, Milo Martin, Peter Sewell, Derek Williams. An Axiomatic Memory Model for POWER Multiprocessors. CAV 2012, 2012. doi:10.1007/978-3-642-31424-7_30
- Jade Alglave, Luc Maranget, Michael Tautschnig. Herding Cats: Modelling, Simulation, Testing, and Data Mining for Weak Memory. ACM TOPLAS, 2014. doi:10.1145/2627752