Buffered Memory Model BMM
A pragmatic, TSO-style buffered memory model proposed as a candidate for Java, motivated by building a verified JVM in the spirit of CompCertTSO rather than fully replacing the JMM. Each thread has a store buffer, so the principal relaxation over SC is store→load reordering. The authors proved the external DRF theorem and the soundness of several program transformations, and modified an open-source JVM to preserve BMM at roughly 1% average overhead on x86.
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
- no Armv7
- no Armv8
- Reordering sound
- yes Store→Load
- no Store→Store
- no Load→Load
- no Load→Store
- Elimination sound
- yes Store/Load
- yes Store/Store
- yes Load/Load
- no Load/Store
- Other local transformations
- yes Irrelevant load elim.
- yes Speculative load intro.
- no Roach motel
- yes Trace preserving
- no Common subexpr. elim.
- Global transformations
- no Thread inlining
- Reasoning guarantees
- yes External DRF
- yes Coherence
- yes No undefined behaviour
- yes In-order execution
- yes No out-of-thin-air
Ordering relationships
- Strictly weaker than
- Sequential Consistency (SC) — BMM equips each thread with a store buffer, so the store→load (SB) outcome becomes observable; SC forbids it.
- Equivalent to
- Total Store Order (TSO) — BMM is a pragmatic TSO-style buffered model proposed as a candidate Java memory model; on the store-buffer relaxations it coincides with TSO.
References
- Delphine Demange, Vincent Laporte, Lei Zhao, Suresh Jagannathan, David Pichardie, Jan Vitek. Plan B: A Buffered Memory Model for Java. POPL 2013, 2013. doi:10.1145/2429069.2429110
- Evgenii Moiseenko, Anton Podkopaev, Dmitrii Koznov. A Survey of Programming Language Memory Models. Programming and Computer Software 47(6), pp. 439–456, 2021. doi:10.1134/S0361768821060050