Hi folks,
We have been working on the notion of causal loops and we think we have
come up with a solution. This is still preliminary, but please look over it.
We think that this rule will eliminate the need for an additional
separate rule (formal or informal) forbidding causal loops.
Consider an execution E with a PUR read r of a write w.
The PUR r must be validated by a subsequence S of E s.t. S does not
contain r, and S contains its own backwards slice. A backwards slice from
a read in a program includes all of the instructions that influence
whether control reaches that point, and all of the instructions that
influence the value read by it.
S must have the property that in all executions E' s.t. S is contained in E',
* both a read r' and the write w occur, where r' corresponds to the
same statement as r and reads the same variable as r, but may see the
value of a different write, and
* r' and w are unsynchronized with respect to each other.
So, let's take something inspired by Sarita's example:
Initially, X = Y = 0 and K is equal to either 1 or 2
Thread 1
if ((X == 1) || (K == 1)){
Y = 1
}
Thread 2
if (Y == 1) {
X = 1
}
When the initial condition is K=2, there are no data races. So we
want to guarantee sequentially consistent semantics when K=2, which
will prohibit the result K=2, X=1, Y=1.
Under our old model, an execution trace with K=2 and a PUR of Y seeing the
value 1 could be validated by an execution trace with K=1 in which the
write Y=1 does occur before the read of Y.
Under the new model, the only subsequences which guarantee that the write
Y=1 occurs and the read of Y occurs are those subsequences which include
K=1. Thus, the PUR of Y seeing the value 1 cannot be validated in any
execution trace in which K=2.
Here's another example that was giving us trouble:
Thread 1:
r1 = x
r2 = r1*r1 - r1 + 1
y = r2
Thread 2:
r3 = y
r4 = r4*r4 - r4 + 1
x = r4
In this example, we want to be able to have a PUR read of x in thread
1 see the write to x of 1 by thread 2. Here, S can be the empty
subsequence. In all executions containing the empty subsequence
(i.e., in all executions) both the read and write occur, and they are
not synchronized with respect to each other.
-------------------------------
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