**Next message:**Bill Pugh: "RE: JavaMemoryModel: Comments on Sarita's example for our model, and on Sarita's model"**Previous message:**Sarita Adve: "RE: JavaMemoryModel: Comments on Sarita's example for our model, and on Sarita's model"**Next in thread:**Sarita Adve: "RE: JavaMemoryModel: Our latest trial balloon"**Reply:**Sarita Adve: "RE: JavaMemoryModel: Our latest trial balloon"**Messages sorted by:**[ date ] [ thread ] [ subject ] [ author ]**Mail actions:**[ respond to this message ] [ mail a new topic ]

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

**Next message:**Bill Pugh: "RE: JavaMemoryModel: Comments on Sarita's example for our model, and on Sarita's model"**Previous message:**Sarita Adve: "RE: JavaMemoryModel: Comments on Sarita's example for our model, and on Sarita's model"**Next in thread:**Sarita Adve: "RE: JavaMemoryModel: Our latest trial balloon"**Reply:**Sarita Adve: "RE: JavaMemoryModel: Our latest trial balloon"**Messages sorted by:**[ date ] [ thread ] [ subject ] [ author ]**Mail actions:**[ respond to this message ] [ mail a new topic ]

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