Next: Reality Up: Fixing the Java Memory Previous: Introduction

Subsections

The Java Memory Model

In this section, I try to interpret JMM, the existing Java Memory Model, as defined in Chapter 17 of the Java Language Specification [GJS96]. The same definition also appears in Chapter 8 of the Java Virtual Machine Specification [LY96].

A number of terms are used in the Java memory model but not related to Java source programs nor the Java virtual machine. Some of these terms have been interpreted differently by various people. I have based my understanding of these terms on conversations with Guy Steele, Doug Lea and others.

A variable refers to a static variable of a loaded class, a field of an allocated object, or element of an allocated array. The system must maintain the following properties with regards to variables and the memory manager:

It must be impossible for any thread to see a variable before it has been initialized to the default value for the type of the variable.
The fact that a garbage collection may relocate a variable to a new memory location is immaterial and invisible to the memory model.

The existing Java memory model discusses use, assign, lock and unlock actions:

A use action corresponds to a getfield, getstatic or array load (e.g., aaload) Java bytecode instruction.
An assign action corresponds to a putfield, putstatic or array store (e.g, aastore) Java bytecode instruction.
A lock action corresponds to a monitorenter Java bytecode instruction.
A unlock action corresponds to a monitorexit Java bytecode instruction.

Bug fixes

The JMM suggests that at thread termination, a thread doesn't need to write back the results of assigns to main memory. This is obviously (to me) a bug and I assume it is fixed by saying that there must be a store associated with the last assign to a variable in a thread.

The JMM also doesn't force a thread to pushed cached writes out to main memory before starting a new thread. This has been acknowledged as a bug.

Interpretation

Due to the double indirection in the Java memory model, it is very hard to understand. What features does it provide?

**Figure 1:** Execution valid for Java only due to prescient stores
$\begin{figure}\begin{center} \begin{tabular}{\vert c\vert c\vert} \multicolumn{... ...lumn{2}{c}{Anomalous result: a = 1, b = 1} \end{tabular}\end{center}\end{figure}$

**Figure 2:** Actions and orderings for Figure 1 without prescient stores (with prescient stores, delete orderings from assign actions to store actions)
$\begin{figure}\centerline{\epsfxsize=3in \epsfbox{ps1.eps}} \end{figure}$

**Figure 3:** Example showing that reads kill
// p and q might be aliased int i = p.x // concurrent write to p.x // by another thread int j = q.x int k = p.x

Consider the example in Figure 1. Gontmakher and Schuster [GS97] state that this is an execution trace that is illegal for Java, but they are incorrect because they do not consider prescient stores [GJS96, §17.8]. Without prescient stores, the actions and ordering constraints required by the JMM are shown in Figure 2. Since the write of y is required to come after the read of x, and the write of x is required to come after the read of y, it is impossible for both the write of x to come before the read of x and for the write of y to come before the read of y.

With prescient stores, the store actions are not required to come after the assign actions; in fact, the store actions can be the very first actions in each thread. This makes it legal for the write actions for both x and y to come before either of the read actions, and for execution to result in a = b = 1.

What the JMM does require is Coherence [ABJ⁺93]. Informally, for each variable in isolation, the uses and assigns to that variable must appear as if they acted directly on global memory in some order that respects the order within each thread (i.e., each variable in isolation is sequentially consistent). A proof that the Java memory model requires Coherence is given in [GS97]. That paper didn't consider prescient stores, but it doesn't impact the proof that the JMM requires Coherence; even with prescient stores, the load and store actions for a particular variable cannot be reordered.

In discussions, Guy Steele stated that he had intended the JMM model to have this property, because he felt it was too non-intuitive for it not to. However, Guy was unaware of the implications of Coherence on compiler optimizations (below).

Coherence means that reads kill

Consider the code fragment in Figure 3 Since p and q only might be aliased, but are not definitely aliased, then the use of q.x cannot be optimized away (if it were known that p and q pointed to the same object, then it would be legal to replace the assignments to j and k with assignments of the value of i). Consider the case where p and q are in fact aliased, and another thread writes to the memory location for p/q.x between the first use of p.x and the use of q.x; the use of q.x will see the new value. It will be illegal for the second use of p.x (stored into k) to get the same value as was stored into i. However, a fairly standard compiler optimization would involve eliminating the getfield for k and replacing it with a reuse of the value stored into i. Unfortunately, that optimization is illegal in any language that requires Coherence.

One way to think of it is that since a read of a memory location may cause the thread to become aware of a write by another thread, it must be treated in the compiler as a possible write.

In talking with a number of people at OOPSLA98, I found that most people were not aware of the implications for compilers of Coherence in the JMM, and at least one shipping commercial Java compiler violates Coherence.

**Figure:** Counter example to JMM $\equiv$ Coherence
// p and q might be aliased int i = r.y int j = p.x // concurrent write // to p.x by another thread int k = q.x p.x = 42

**Figure 5:** JMM actions for Figure 4
$\begin{figure}\centerline{\epsfxsize=3in \epsfbox{jmm1.eps}} \end{figure}$

JMM is stronger than Coherence

Initially, I tried to derive a proof that, excluding locks and volatile variables, the Java memory model is exactly Coherence. Instead, I came up with a counter-example. Consider the code fragment in Figure 4, and the scenario in which p and q are aliased (although we are not able to prove it), and another write happens to update the value of p/q.x between the read of p.x and the read of q.x, so that the use of p/q.x sees a different value than the use of p.x. The actions corresponding this execution, and their ordering constraints, are shown in Figure 5.

The boxes and arrows in this diagram arise for the following reasons:

a

[GJS96, §17.3, bullet 1]: All use and assign actions by a given thread must occur in the order specified by the program being executed.

b

[GJS96, §17.3, bullet 4]: ... must perform a load before performing a use

c

Since the use of p/q.x sees a different value than the use of p.x, there must be a separate load instruction for the use of p/q.x, which must precede the use of p/q.x and follow the use of p.x.

d

[GJS96, §17.8, bullet 3]: No load of V intervenes between the relocated [prescient] store and the assign.

e

[GJS96, §17.3, second list of bullets, 1st bullet]: For each load, there must be a corresponding preceding read

f

[GJS96, §17.3, second list of bullets, 2nd bullet]: For each store, there must be a corresponding following write

g

[GJS96, §17.2, 2nd bullet]: actions performed by main memory for any one variable are totally ordered

[GJS96, §17.3, second list of bullets, 3rd bullet]: edges between load/store actions on a variable V and the corresponding read/write actions cannot cross

h

Since we consider the situation where p and q are aliased and the use of p/q.x sees a different value than the use of p.x, there must have been an intervening write to p.x by another thread between the load of p.x and the load of p/q.x.

**Figure 6:** JMM actions for Figure 4 after re-ordering use of r.y and use of p.x
$\begin{figure}\centerline{\epsfxsize=3in \epsfbox{jmm2.eps}} \end{figure}$

I showed this example to Guy Steele and he tentatively agreed that the JMM imposed the constraints shown in Figure 5, although he did not double check it at length.

This ordering constraints was definitely not intended, and has a substantial impact on optimizing Java compilers and on Java programs running on aggressive processor architectures.

Reorderings are not closed under composition

In Figure 5 it would be legal for the read r.y action to occur after the read p.x action. But if we tried to perform this transformation at the bytecode level (moving the getfield r.y instruction to after the getfield p.x action), we get the actions shown in Figure 6. In these set of actions, it would be legal to perform the read r.y action after the write p.x action. So the set of legal transformations on Java programs are not closed under composition. You can't perform a transformation at the bytecode level without reasoning about whether or not there might exist any downstream component that might perform a reordering that, when composed with your reordering, produces an illegal reordering of the memory references.

This pretty much prohibits any bytecode transformations of memory references.

There may be other strange constraints imposed by the existing JMM, but at this point we switch from trying to decipher the existing JMM to deciding what features we want in a new Java memory model.

Next: Reality Up: Fixing the Java Memory Previous: Introduction

William Pugh