JavaMemoryModel: Relaxing formalization of "causal loop" safety

From: Bill Pugh (pugh@cs.umd.edu)
Date: Mon Jul 15 2002 - 10:49:24 EDT


SUMMARY:
For some time, I've said that the new Java memory model should
enforce something vaguely described as "out-of-thin-air" safety for
incorrectly synchronized programs.

"Out-of-thin-air" safety requires that every read of a variable v see
the value written by some write to v. Now, because there is no simple
global clock, we can't require that a read see the value written by a
_previous_ write. However, we also want to avoid causal loops, in
which an event causes/justifies itself.

For example, in

Ex 1:
Initially, x = y = 0

Thread 1 Thread 2
r1 = x r2 = y
y = r1 x = r2

We want to forbid any result other than r1 = r2 = 0. Without some
kind of guard against causal loops, you could argue that r1 = r2 = 42
is a valid answer. The reasoning is that each read is seeing the
value of some other write to the corresponding variable, and that the
actions of each thread are consistent with the values read by the
thread.

Due to difficulties in defining what a causal loop is and possible
interference with advanced compiler optimizations. I am proposing a
philosophical change in the Java memory model. Rather than forbid all
causal loops in the formal specification, the formal specification
will forbid only some of the most outrageous cases of causal loops.
There will also be an informal statement that VM's should not allow
any causal loops. Since a VM would have to work perversely and hard
to exhibit a causal loop, I think this will suffice.

This change is necessary for revisions that Jeremy and I have made to
our model to fix various problems.

DETAILS

One way to avoid causal loops is as Sarita did. Define dependences
between statements, and require that the dependence graph be acyclic.
The problem with this is whether statement Y is dependent upon
statement X is dependent on the semantics of the program. And you
can't use the semantics in defining the memory model, since the
semantics depends upon the memory model.

An example of the cases this approach has problems with in Ex 2:

Ex 2:
Initially, x = y = 0

Thread 1:
r1 = x
r2 = r1*r1 - r1 + 1
y = r2

Thread 2:
r3 = y
r4 = r4*r4 - r4 + 1
x = r4

Can this program result in r1 = r3 = 1?

The problem is that a compiler might perform an analysis that
determines that x and y are always 0 or 1, and therefore determine
that r2 and r4 are always 1, and reorder the writes, allowing r1 = r3
= 1.

A dependence based approach is particularly tricky because exceptions
make almost every statement control dependent upon all previous
statements that could throw exceptions.

The alternative to this is something like the prescient writes in the
original memory model. In earlier versions of our semantics, we also
used prescient writes (correspond to a write which has a
corresponding initWrite operation). In order to avoid causal loops,
we required that initWrites be guaranteed: that at the time the
initWrite occurs, that the program be guaranteed to perform the write
in all possible execution paths.

Now, this kept on getting us into trouble. We had to introduce
guaranteedReads, which nobody was happy with. And then we found other
problems.

Ex 3:
Initially, x = y = z = 0

Thread 1:
x = 1

Thread 2:
r1 = z
r2 = x
y = r2

Thread 3:
r3 = y
z = r3

The question in, can this program result in r1 = 1?

For this to happen, under our earlier semantics, we would need to
perform an initWrite of y=1 in thread 2 before the read of x.
However, at this point the initWrite can't be guaranteed, because the
read of x by thread 2 might see the value 0, causing 0 to be written
to y.

So, we've been struggling with causal loops ever since the very
beginning of this effort, and for the past two months we knew the
solutions at hand didn't work.

So, at this point there are four possible options:

a) Use a rule forbidding dependence cycles, knowing that this could forbid
   certain compiler optimizations.

b) Use a double semantics approach. Have one memory model that is used for
    deciding whether something is a causal loop, and another memory model
    for execution that using the causal loop definitions from the other
    semantics. (Essentially what Sarita suggested a week ago).

c) Hope that somebody will have a breakthrough in the design of memory
   models in the very immediate future.

d) Relax the formalization of the causal loop aspect of "not out of thin air"
    safety. The specification will still say that all causal loops are
    prohibited, but only some causal loops will be prohibited by the formal
    rules of the specification, due to the difficulty in formally defining
    causal loops.

As you can probably guess, I am now going to recommend d.

I am not happy with choices a or b, and we can't depend upon c
happening when we need it to, if ever.

I believe we can come up with adequate formal safeguards to eliminate
the most outrageous causal loops (e.g., seeing r1 = r2 = 42 in Ex 1)
and capture the most important safely properties related to causal
loops. Also, a causal loop could occur in practice only if some
perverse VM went out of its way to introduce it, and I'm not sure how
hard we need work to prevent perversely bad VM's. After all, we write
off many other more significant issues as quality of service issues.

So I'm proposing that the formal semantics allow incorrectly
synchronized programs to exhibit anomalous behavior that can only be
explained by a causal loop. For example, the current rules I'm
considering for "out-of-thin-air" safety would still allow the
following to squeak by the formal version of the rules:

Ex 4:
Initially, x = y = z = 0

Thread 1:
z = 2

Thread 2:
r1 = z
x = r1

Thread 2:
r2 = x
r3 = r2 + 1
y = r3

Thread 3:
r4 = y
r5 = r4 - 1
x = r4

Causal loop behavior: r1 = 0, r2 = 2, r4 = 3

The formal rules will forbid Ex 3, because they will require that
each value be created somewhere. However, this rule still allows Ex 4.

Now, while this is distasteful, I don't think it impairs the ability
of people to write reliable software. And we can debate the exact set
of rules used to rule out the blatant causal loops. But since this
is a significant change in the philosophy of the proposed memory
model, I want to talk about this change at the high level before we
get down to the details.

        Bill

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



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