Re: JavaMemoryModel: Isolation properties in the JMM

From: Doug Lea (dl@cs.oswego.edu)
Date: Sun Feb 01 2004 - 08:36:54 EST


> It feels like you're trading on the obvious
> reasonableness of the the much weaker property "For _every_ execution E
> of a program ...".

This turns out to be a STRONGER property, at least in the sense that
people/models have framed it. It takes a lot of backing up to explain:

Among the goals here is to provide the weakest model/spec that does
not allow unacceptable behaviors. All other things being equal, weaker
is better because it allows compilers and processors to better
optimize execution. The weakest conceivable model would require only
happens-before consistency. However, we've seen that this would allow
clearly unacceptable behaviors such as "out of thin air" reads. Note
that these kinds of problems only occur in the presence of
circularities etc., as seen in the test cases at
http://www.cs.umd.edu/~pugh/java/memoryModel/CausalityTestCases.html
for which traditional sequential programming language semantics offer
no guidance, and which are hard to think about. But still, we need to
ensure that the model is free of anomalies even in these weird cases
so as to guarantee that basic Java safety properties are preserved.

As several people have now noticed, allowing the behavior in test case
10 (pasted here for convenience) introduces a potential anomaly that
you can think of as a subtle variant of the out-of-thin-air problem:

Causality test case 10

  Initially, x = y = z = 0

  Thread 1:
  r1 = x
  if (r1 == 1)
    y = 1

  Thread 2
  r2 = y
  if (r2 == 1)
    x = 1

  Thread 3
  z = 1

  Thread 4
  r3 = z
  if (r3 == 1)
    x = 1

  Behavior in question: r1 == r2 == 1, r3 == 0.

To see the issue, compare this to a version involving only Threads 1 and 2:

  Initially, x = y = 0

  Thread 1:
  r1 = x
  if (r1 == 1)
    y = 1

  Thread 2
  r2 = y
  if (r2 == 1)
    x = 1

  Behavior in question: r1 == r2 == 1.

which is clearly forbidden.

Under some possible underlying models, adding Threads 3 and 4 can
cause the answer to change because a compiler/processor could decide
that because there is SOME execution of the program that writes 1 to
x, then both r1 and r2 can be 1. However, this execution clearly won't
happen if r3==0 (in Thread 4), which is the behavior in question.

Some people think the behavior in case 10 should be forbidden because
it produces values that appear to just be "guesses", especially when
viewed by a programmer who knows of the existence of Threads 1 and 2,
but not 3 and/or 4. Other people don't think this is a big deal; that
it is surprising but not something that has to be ruled out. But Bill,
Victor, and others have offered variants of case 10 that get
uncomfortably close to being safety concerns. Frustratingly, no one
has been able to come up with a decisive example where this could
cause a real security lapse. But being conservative in the face of
uncertainty, we want to characterize exactly what the problem is, and
either show that it cannot lead to insecurities or ensure that the
underlying model does not allow it.
 
The isolation property Bill posted is our current best shot at
characterizing this at a high enough level to be able to explore and
discuss it. As Bill said, this property is not likely to be primitive
property of any model, but a derived one. For example, a model that
only allowed prescient/speculative writes when they are known to occur
across all possible executions seems to have this property, but some
people (including, I think, Sarita) believe that this would otherwise
be too strong a constraint, that would disable some desirable
optimizations.

In any case though, the main issue we (speaking for JSR-133) want
feedback on is whether the isolation property is necessary, desirable,
and well-formed enough to use as a basis for evaluating options.

-Doug

-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel



This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:57 EDT