Causality and Out-of-Thin-Air Values in the Java Model

Two threads each read a variable and write the value they read to another variable, which the first thread then reads. There is no synchronisation, no initial value other than zero, and no write of 42 anywhere in the program. Yet a memory model built only from happens-before consistency can justify the outcome in which both threads read 42.

The justification is a self-supporting cycle: thread 0 reads 42 from y because thread 1 wrote 42 to y, and thread 1 wrote 42 to y because it read 42 from x, and thread 0 wrote 42 to x because it read 42 from y. Each read is justified by a write that is itself justified by the read. Nothing outside the cycle introduces the value. This is an out-of-thin-air value, and eliminating it is the reason the Java Memory Model is built on causality rather than on happens-before consistency alone.

Why happens-before consistency is not enough

The happens-before consistency rule says that a read must not see a write that happens after it, and must not see a write that is overwritten by another write that happens before the read. In the cycle above, no read sees a write that happens after it: the writes and reads are all concurrent, so no happens-before edges connect them at all. The rule is satisfied, and the outcome is permitted.

Every relaxed model has this problem in some form, and the standard answer is a causality constraint: the values in an execution must be justifiable by a finite sequence of steps, each of which commits a read and a write that are already justified. A value that only exists because of a cycle with no external source is rejected.

The formulation in the Java Memory Model is a commitment order. An execution is valid if there is a sequence of “committing” actions, starting from the actions of the program’s initial state, such that each committed read sees a write that is already committed or is itself part of the same commit step, and the whole execution is committed by the end. The cycle above has no starting point, so no commitment sequence exists, so the execution is invalid.

The causality requirements, informally

The specification states the requirement in a form that is deliberately operational rather than declarative, because a purely declarative formulation turned out to be either too weak or too strong.

The rules are usually summarised in terms of “committing” a set of actions. A set of actions may be committed if every read in the set sees a write that is either committed already or in the set, and the set is consistent with the program order and with the synchronisation order. The execution is valid if the entire set of actions can be committed by repeated application of this rule, starting from the empty set.

The subtlety that makes the definition work is that a commit step may include both a write and the read that justifies it, provided the pair is internally consistent. That allows speculative-looking executions — where a read sees a write that is itself only justified by that read — as long as the pair can be committed together and the rest of the execution follows. It is this allowance that makes the model permissive enough to accept real optimisations while rejecting the pure cycle.

The definition is also known to be unsatisfying in one respect: it is not a simple set of constraints on the execution graph, and reasoning about it requires constructing the commitment sequence. Later work on the C++ model used a different approach, and the difference between the two is instructive.

What the Java model does differently from C++

The C++ model’s answer to out-of-thin-air is a coherence-based constraint on atomic objects together with a rule intended to exclude cycles that have no external justification. It is not fully satisfactory either: the standard’s wording is widely regarded as an approximation, and an implementation is permitted to forbid executions the letter of the standard would allow. The practical guidance for both languages is the same — write synchronised code and do not depend on the fine points of the relaxed-atomic rules.

The Java model predates C++11 and influenced it, but the two differ in scope. Java’s model covers fields of objects, array elements, and volatile variables, with volatile providing sequential consistency for the volatile accesses and the happens-before edges around them. Ordinary field access in Java is not atomic in the sense of C++‘s relaxed atomics — it has no ordering guarantee at all, but it also has no undefined behaviour: a racy read returns some value that was written, never a value that was never written.

That last property is the practical difference. Java’s racy programs are not undefined; they are merely unpredictable. A long field that is not volatile may be read as a torn value on some implementations, and the specification’s rules for long and double explicitly permit that, but the value is still a combination of writes that occurred. C++‘s racy programs are undefined, which is a stronger statement and permits stronger optimisation.

Volatile, final, and the edges Java does provide

Java’s volatile is sequentially consistent: a volatile write happens-before a subsequent volatile read of the same variable, and all volatile accesses in the program are totally ordered. The practical effect is that a volatile flag and a plain data field form a valid publish protocol. Java has no relaxed or acquire-release alternative to volatile on ordinary fields, so the ordering is attached to the variable’s declaration rather than chosen per operation — the one structural difference from the C++ atomic types, where the ordering is an argument to each access.

final fields get a special rule. A field declared final and written in a constructor is guaranteed to be visible to any thread that obtains a reference to the object, without synchronisation. The guarantee is implemented by a freeze action at the end of the constructor, and the compiler must not let the reference escape before the freeze. This is what makes immutable objects safe to share without locks, and it is the reason final is load-bearing for correctness rather than merely a documentation aid.

The freeze rule has a well-known loophole: if the reference to the object escapes during construction — stored into a static field, passed to another thread — the other thread may see the object before the freeze, and the final fields may not be initialised. This is why constructors that publish this are a bug even when the fields are final.

Where the model still has holes

The causality requirements are the least declarative part of the Java specification. They are stated as rules for building a commitment sequence rather than as constraints that can be read off an execution graph, and the practical guidance that follows is to avoid depending on their fine points.

That operational style is the main limitation. Proving that a particular execution is valid means exhibiting a commitment sequence for it; proving one invalid means showing that no sequence reaches it. The argument is tractable for small examples, which is how the model’s corner cases were argued, but it does not scale to reasoning about a whole program, and it is the reason later work on other language models reached for graph-shaped constraints instead.

Implementations are also permitted to be stricter than the rules. A compiler may forbid an execution the commitment rules would admit, as long as every execution it does permit is one the rules allow, and that latitude is what makes the model implementable for compilers that optimise while the program runs.

A second constraint pulls in a different direction: the synchronisation order, the total order over all synchronisation actions, which fixes the relative position of volatile accesses and monitor operations. Any execution the rules admit has to be consistent with both that order and the happens-before relation, and the two describe different things — one is a global sequence of the operations that synchronise, the other is a partial order carrying the value-justification argument. Holding both fixed while a commitment sequence grows is the fiddly part of applying the definition.

What the model is for

The Java Memory Model’s complexity is not incidental. It exists because Java needed a single specification that would permit the optimisations real JIT compilers perform — reordering, caching in registers, eliminating redundant reads — while guaranteeing that correctly synchronised programs behave sequentially consistently. The DRF-SC guarantee is the same promise C++ makes, and Java’s version has to hold for a language where the compiler runs at the same time as the program and can therefore make optimisations a static compiler cannot.

The cost of that permissiveness is a specification that is difficult to reason about at the edges and that leaves some executions to the implementation’s discretion. The alternative — a stricter model — would forbid optimisations that JIT compilers depend on, and the performance cost of that was judged unacceptable. The same trade, in a different form, appears in the Linux kernel’s model, where the constraints are the ones a kernel actually needs and the specification is written to be usable by the people who maintain it.