Relaxed Memory Model Zoo

Memory model
← 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.

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

  • Jeremy Manson, William Pugh, Sarita V. Adve. The Java Memory Model. POPL 2005, 2005. doi:10.1145/1040305.1040336
  • Doug Lea, Jeremy Manson, William Pugh. JSR-133: Java Memory Model and Thread Specification. Java Community Process, 2004.