[jmm-dev] Another way to punt OOTA

[Doug Lea]

On 10/28/2014 09:39 PM, Hans Boehm wrote:
> Here's another conceivable approach.  This sounds somewhat crazy based on
> our prior assumptions, but it may only be mildly crazy, so here goes.

I think some of the details are crazy, but I agree with most of
the broad points:

First, odds are that we will "solve" OOTA and related speculation
constraints, but in a somewhat disappointing way: most likely by
defining a form of "dep" such that (rf U dep) is acyclic, but where
dep may sometimes be undecidable.  Or any of several variations with
similar impact.  Paul et al's N4216
(http://www.open-std.org/JTC1/SC22/WG21/docs/papers/2014/n4216.html)
presents a meta-litmus test along these lines.  With Alan, Peter,
Viktor, and others looking at this from various angles, I'm still
optimistic about discovering a solution straddled by C11 (allowing
OOTA) and JSR133 (disallowing valid transformations). So it still
seems best to imagine that we arrive (out-of-thin-air!) at a core
model that suffices, even if in some cases it includes caveats
along the lines of "read r could be 42 only if P==NP".

> - The argument for providing well-defined behavior for data races in Java
> was based either on the original model of Java, or on the desire to
> unconditionally maintain secondary properties, like memory safety, even in
> the presence of data races.

Yes. No-OOTA is only one part of the minimal guarantees of even
arbitrarily racy Java programs.  This set of predicates forms the Java
analog of C/C++ undefinedness.  Informally, we (in conjunction with
other part of the JLS) need to ensure that nothing anyone can write in
Java proper causes a JVM to crash (with disclaimers about JNI etc that
from a security point of view arbitrarily widen the trusted computing
base.  BTW, this is the main reason we need to stop making people use
Unsafe to get the effects of enhanced-volatiles.)  As I sketched out
last January (mostly on the pre-jmm9 list), we ought to solidify
meanings of memory safety and security -- these are at least as
important as guaranteeing SC for DRF programs. And from there, we need
simple characterizations of at least release->acquire and create->use
(constructors).  But I don't think we can simply characterize all the
intermediate points. It seems impossible to routinely distinguish
subtly correct vs subtly incorrect code. For example you need to know
that the String hash function is idempotent, and that if hash is zero,
it intentionally recomputes, to see that racy lazy initialization of
String.hashCode is OK.


> - We're essentially already making the preceding dubious assumption.  We
> have all sorts of library APIs that don't specify how they behave in the
> presence of races, but only say that you shouldn't do that.  We're somehow
> supposed to conclude that the heap can't be corrupted even in the presence
> of racy library calls, because of the (unstated?) assumption that libraries
> should behave as though they were implemented in Java, and Java programs
> preserve e.g. memory safety.

To emphasize: I agree.

>
> - Switch to a much more C++-like (or Java library-like) model in which data
> races have something like "undefined behavior".  Exactly how to model that
> is an open question.  Ordinary loads can only see stores that happen-before
> them, but racing loads trigger "undefined behavior". "Undefined behavior"
> should be defined to allow reporting an error and produce any type correct
> answer for the racing load.

And to emphasize: I disagree in the general case because I don't
know how to do it. However, I don't think there is anything stopping
JVM+core-libraries conspiring to throw exceptions in particular
kinds of races that are never correct. Or for add-on tools to
dynamically or statically detect them.

>
> - [Probably challenging, others understand the Java constraints better than
> I] Introduce a mechanism for (nearly) unordered memory-order-relaxed like
> racing loads.  Require current racing accesses to use that mechanism
> instead.  (Open question: coherence)

I have yet to see a compelling example/case for guaranteeing coherence
for relaxed accesses to volatiles (i.e., in Java 9+, the
enhanced-volatile mechanism for a relaxed read.)

-Doug