Relaxed Memory Model Zoo

Relaxed Memory Order (RMO)
← Back to the map

Relaxed Memory Order RMO

1994 · SPARC International · hardware

The weakest SPARC model. Allows all four reorderings (load-load, load-store, store-load, store-store) between independent memory operations.

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
  • yes Load→Load
  • yes Load→Store
Reasoning guarantees
  • yes Coherence
  • yes No undefined behaviour
  • no In-order execution
  • yes No out-of-thin-air
Atomicity guarantees
  • yes Multicopy atomic

Ordering relationships

Strictly weaker than
Strictly stronger than
  • Cache Coherence — RMO still enforces per-address coherence; weaker models could violate it.
  • DEC Alpha Memory Model — SPARC RMO preserves address/data/control dependencies; DEC Alpha uniquely relaxes dependent-load ordering (Alglave, Maranget & Tautschnig, Herding Cats, TOPLAS 2014, p.18) and is non-multi-copy-atomic. Separating outcome: MP+dmb+addr, forbidden by RMO (address dependency preserved), allowed by Alpha (dependent loads not ordered) — machine-run under herd7 against a portable abstract-alpha.cat (RMO Never 0 3, Alpha Sometimes 1 3). Containment is the litmus-tier monotonicity argument: Alpha relaxes strictly more than RMO (dependencies; store atomicity) and no less on any axis, so Alpha ⊆ RMO, strict by the witness. See litmus/strictly-weaker/RMO-vs-Alpha.

References