The JMM Cookbook for Java Developers

Note: This cookbook is not currently known to be correct. It is a hopeful draft. Treat it as such.

Doug Lea's JSR-133 Cookbook for Compiler Writers (aka "the JMM cookbook") describes a set of implementation rules that is sufficient for meeting the JMM specification. The cookbook is an amazingly useful tool for Compiler Writers and JVM implementers, which is it's stated purpose. It describes a set of implementation rules that is sufficient for meeting the JMM specification, and is used by most JVMs, most of the time. The simple ordering matrices described provide great guidelines that are easy to follow and reason about.

However, being a sufficient-but-not-necessary set of rules, this Compiler Writer's JMM Cookbook does not provide Java developers with a tool to reason about the rules that are *guaranteed* to be followed by any JVM compliant with the JMM specification. While many JVM implementations follow these cookbook rules in order to meet the JMM specification, it can be dangerous for Java developers to assume that the rules stated are guarantees, a JVM implementations that meet the JMM specification but use more relaxed rules that stated in the JMM cookbook are certainly possible. The barrier matrices in the cookbook, as easy as they are to understand and follow, are not a reliable predictor of what JVMs will actually do now or in the future.

This leaves Java developers with the JMM specification itself, which is unfortunately not reliably parse-able by mortals on a daily basis. Applying JMM spec criteria to code requires a level of transcendent meditation that is not only hard to achieve, but more importantly hard to maintain, making it impractical for daily reference use by programmers that want to actually construct "safe" code. This is most easily evidenced by the occasional storms of e-mails and mailing list disagreements among people who actually spend much of their time specifying, implementing, and testing memory models.

So What's a Java developer to do?

Gil's expanded barrier table

I've been playing with an attempt to describe the required (rather than just a sufficient) reordering limitations that result from the JMM spec in a way that can be more readily consumed by Java developers that want to reason about their own programs, and to understand the guarantees provided to them by the JMM.

I believe that the following matix, using Doug's convenient format, describes required (rather than simply sufficient) reordering rules between the common operations of Load, Store, Volatile Load, Volatile Store, Monitor Enter, and Monitor Exit.

The matrix uses Doug's original notation for LoadLoad, LoadStore, StoreStore and StoreLoad barriers used in the JMM cookbook's most commonly referred to matrix, in addition to his expanded use of the following: LoadExit, StoreExit, EnterEnter, EnterExit, ExitExit, ExitEnter, EnterLoad, EnterStore. Into that mix, We throw in the additional "VLoad" and "VStore" notation to expand the set with LoadVStore, LoadVLoad, StoreVStore, VLoadLoad, VLoadStore, VLoadVLoad, VLoadVStore, VLoadEnter, VLoadExit, VStoreVLoad, VStoreVStore, VStoreEnter, VStoreExit, ExitVLoad, ExitVStore.

I believe that Fully expanding to explicitly address ordering rules for Loads, Stores, Volatile Loads, Volatile Stores, Monitor Enter and Monitor Exit disentangles to:

Plus the special final-field rule requiring StoreStore and StoreVStore barriers in:
      x.finalField = v; StoreStore; sharedNonVolatileRef = x;
      x.finalField = v; StoreVStore; sharedVolatileRef = x;

To be clear about both the purpose and utility of this matrix: This matrix is NOT an attempt to capture a precise description of the JMM. Instead, it is intended to be less-or-equal to the JMM in strictness, with every single barrier in the matrix being absolutely required by the JMM, but with some JMM rules not necessarily being captured. If the matrix achieves this goal, developers can safely assume that all the reordering rules stated in it are actually followed by all JVMs that comply with the JMM. It is certainly possible that (and acceptable for) the JMM to be more strict than the rules described in the matrix. It is certainly possible for JVMs to be more strict.

I hold some *hope* that either the current or a future JMM spec guarantees every single one of the orderings in the above matrix. Since the orderings stated can be reasoned above in a transitive fashion, they provide a convenient recipe for developers to follow in determining which reorderings are impossible in their code.

We now embark on trying to show how each of the above reorderings is guaranteed by the JMM specification: This exercise is left for the reader ;-).

Starting on that exercise though, much of the matrix can simply be attributed to this single statement in the JMM specification (17.4.4):
"Every execution has a synchronization order. A synchronization order is a total order over all of the synchronization actions of an execution. For each thread t, the synchronization order of the synchronization actions (17.4.2) in t is consistent with the program order (17.4.3) of t."
To my current understanding, this single statement, on it's own, covers the bottom right 4x4 part of the matrix, requiring each of the barriers stated between any combination of a Volatile Load, Volatile Store, Monitor Enter, and Monitor Exit (all of which are synchronization actions per (17.4.2)).

This leaves us with only 8 other barriers to prove. I worry that they may require adding "specific variable" statements to be actually required...