Relaxed Memory Model Zoo

Java Memory Model (JMM)
← Back to the map

Java Memory Model JMM

2005 · Manson, Pugh, Adve · language, formal, standard

Formalised in JSR-133. Defines happens-before (HB) based on synchronisation actions. Provides DRF-SC guarantee. Known for complexities around causality and out-of-thin-air values.

Properties

Property vector survey-sourced — from Tables 1–2 of the Moiseenko et al. survey, except cells that cite a specific source.

Compilation optimal mapping to
  • yes x86
  • no POWER
  • yes Armv7
  • yes Armv8
Reordering sound
  • yes Store→Load
  • yes Store→Store
  • yes Load→Load
  • yes Load→Store
Elimination sound
  • yes Store/Load
  • yes Store/Store
  • no Load/Load
  • no Load/Store
Other local transformations
  • yes Irrelevant load elim.
  • no Speculative load intro.
  • no Roach motel
  • yes Trace preserving
  • no Common subexpr. elim.
Global transformations
  • no Thread inlining
Reasoning guarantees
  • yes External DRF
  • no Coherence
  • yes No undefined behaviour
  • no In-order execution
  • yes No out-of-thin-air

Ordering relationships

Strictly weaker than
Incomparable with
  • OCaml Memory Model (OCaml MM) — Both are language-level models providing DRF-SC but with different treatments of racy accesses.
  • Java Access Modes (JAM) — JAM is a proposed revision of the JMM built on VarHandle access modes (plain/opaque/release-acquire/volatile); it strengthens the treatment of atomics via RC11 while differing from the original JMM's causality machinery, so neither contains the other.
  • Operational Happens-Before Model (OHMM) — OHMM is an operational attempt to repair the JMM — a global event buffer with a replay mechanism, tracking syntactic dependencies to forbid thin-air. It restructures the JMM's semantics rather than strictly refining it, so the two are incomparable.

References

Open JMM in the interactive map →