Jeremy and I are working on a change that addresses the issue raised
by Sarita. I hope our fix will also address the concern some people
expressed about informal prohibitions against causal loops. We hope
to have something ready to post tomorrow.
Part of the problem is that proving that a memory model has desirable
properties X, Y and Z doesn't mean the memory model also has
desirable properties A and B. And it is impossible to ensure that we
have enumerated all of the desirable properties.
Another property that it would be nice to have.
Say you have a program P, and initial condition I1 and I2. These
initial conditions might be set from the command line, environment
variables, or the initialization of the program. Assume that the part
of the program that sets the initial conditions is correctly
synchronized.
Further assume that under initial conditions I1, the entire program
is correctly synchronized. However, under initial conditions I2, the
program is not correctly synchronized.
You would like to have the property that under initial conditions I1,
the program obeys sequentially consistent semantics.
Sarita's proposal doesn't have that property. Consider:
Initially, x = y = 0, foobar = either true or false
Thread 1:
if foobar
x = 1
y = 1
Thread 2:
if x = 1
y = 1
Thread 3:
if y = 1
x = 1
OK, if foobar = true, this program has a data race. However, if foobar=false,
this program is correctly synchronized. However, under Sarita's model
threads 2 and 3 could write to x and y even when foobar=false.
Our previous semantics handles this case, but not other issues with
initial conditions. We hope to handle this in tomorrow's revision.
General comments on Sarita's model. Her first two conditions
essentially give us model A (of the two models I described
previously). Her conditions (3) and (4) are designed further restrict
the model to prohibit causal loops.
However, I don't feel that they are entirely satisfactory.
First, both conditions are intended to do the same thing. If either
condition really captured everything it needed to capture, there
wouldn't be a need for the other condition.
For example, condition (4) doesn't mention control dependence, yet
there is no reason to believe that control dependence is better
handled by (3) than flow dependence.
Condition (4) forces a compiler to reason about possible executions
in a semantics that doesn't include (4) in order to determine whether
a value is truly constant.
Condition (3) has significant problems with contamination across
initial conditions, as I've mentioned. I believe it also suffers from
the problem Sarita mentioned with revision of a week ago; that it
doesn't handle statement splitting transformations.
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:41 EDT