Bill gives a couple of nice, simple examples to try and ferret out
what we mean when we say the CRF JMM ignores control dependence but
respects data dependence for the purposes of reordering. I think it's
pretty clear from these examples that our wording leaves holes wide
enough to drive a truck through. In this case the truck is inventing
values out of thin air...
Let me be more clear, then. Here's a first cut:
1) Reads may be freely reordered across control flow boundaries.
2) A writes may be reordered across a control flow boundary iff it can
be shown that the particular write will occur in any execution.
Here are a couple of simple examples of what is meant in condition 2:
r1 = x
if r1 >= 0
y = 5
x = r1 + 1
else
y = 5
x = r1 - 1
In this case, the assignment to y may be reordered freely; it is
equivalent to either of the following:
r1 = x
y = 5
if r1 >= 0
x = r1 + 1
else
x = r1 - 1
or:
r1 = x
if r1 >= 0
x = r1 + 1
else
x = r1 - 1
y = 5
Indeed, it's always safe by rule (2) to hoist assignments _into_ both
branches of a conditional from _outside_ that conditional. Naturally,
an intervening store may prevent re-ordering:
r1 = x
if r1 >= 0
x = r1 + 1
else
x = r1 - 1
y = x
In this case, the assignment to x may be hoisted into the conditionals
like so, but no further:
r1 = x
if r1 >= 0
x = r1 + 1
y = x
else
x = r1 - 1
y = x
An interesting question at this point is whether we're allowed to
simplify the code for a particular thread based on static information,
and then use that simplification to perform futher reordering. I've
managed to convince myself that hoisting in and out of conditionals
and reordering is sufficient to reason about most of these cases.
> Example 1
>
> Initially, x = y = 0
>
> Thread 1:
> r1 = x
> if r1 >= 0
> y = 1
>
> Thread 2:
> r2 = y
> x = r2
>
> Question: is it legal for this program to result in r1 = r2 = 1?
Answer: no. As written, the assignment to y fails condition (2). We
must execute r1 = x first in thread 1.
Note that if we knew that x was initially 0, we could assume a
particular execution order and replace a local r1 with 0 *everywhere*
in thread 1. (again, I assert this transformation is incorrect unless
all occurrences are eliminated). This would lead to:
Thread 1:
junk = x
y = 1
Thread 2 would remain unchanged.
I'm wracking my brain to come up with a case where we can discharge
the conditional statically, then reorder to permit something odd to
occur, but I cannot do so.
> Example 2
> Initially, x = y = 0
>
> Thread 1:
> r1 = x
> if r1 >= 0
> y = -1
>
> Thread 2:
> r2 = y
> x = r2
>
> Question: is it legal for this program to result in r1 = r2 = -1?
Again, no.
-Jan-Willem Maessen
PS - Note that CSG lost the disk on its main web server containing all
our publications and so forth. Apparently there's been some
difficulty in putting it all back together again. I've put a fresh
copy of the CRF JMM paper in my own web directory here:
http://abp.lcs.mit.edu/~earwig/java-mem.ps.gz
Apologies to anyone who went looking for it at the place where it's
supposed to be. It may be a little while before that gets beaten back
into shape.
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:34 EDT