The Java Memory Model (JMM) is intended to characterize the meaning of
concurrent Java programs. Because of the model’s complexity, however, its
definition cannot be easily transplanted within an optimizing Java compiler,
even though an important rationale for its design was to ensure Java compiler
optimizations are not unduly hampered because of the language’s concurrency
features. In response, the JSR-133 Cookbook for Compiler Writers
(http://g.oswego.edu/dl/jmm/cookbook.html), an informal guide to realizing the
principles underlying the JMM on different (relaxed-memory) platforms was
developed. The goal of the cookbook is to give compiler writers a relatively
simple, yet reasonably efficient, set of reordering-based recipes that satisfy
JMM constraints.

In this talk I will present a formalization of the cookbook which enables the 
validation of the informal recipes which conservatively implement the JMM in the
Power and x86 architectures. Notably, one artifact of our investigation is that
the rules defined by the cookbook for compiling Java onto Power are inconsistent
with the requirements of the JMM, a surprising result, and one which justifies
our belief in the need for formally provable definitions to reason about
sophisticated (and racy) concurrency patterns in Java, and their implementation
on modern-day relaxed-memory hardware.