Relaxed Memory Model Zoo

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.

Equivalent to

• POWER + Transactional Memory (POWER+TM) — Chong, Sorensen & Wickerson (PLDI 2018) add TM rules on top of the POWER consistency axioms (their Fig. 6) that only constrain transactional events; on the non-transactional fragment it coincides with POWER by construction. Validated on a POWER8 machine (no forbidden test observed).
• POWER + DJR Transactions (POWER+DJR) — Dongol, Jagadeesan & Riely (POPL 2018) also instantiate their transactional framework at PPC (POWER); the added transactional axioms only constrain transactional events, so on programs with no transactions the POWER instance coincides with POWER by construction. fragment_restricted: the coincidence holds only on the non-transactional fragment.

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.