**Next message:**David Holmes: "RE: JavaMemoryModel: A simplified version of my model"**Previous message:**Sarita Adve: "JavaMemoryModel: A simplified version of my model"**In reply to:**Bill Pugh: "JavaMemoryModel: Our latest trial balloon"**Next in thread:**Bill Pugh: "RE: JavaMemoryModel: Our latest trial balloon"**Reply:**Bill Pugh: "RE: JavaMemoryModel: Our latest trial balloon"**Messages sorted by:**[ date ] [ thread ] [ subject ] [ author ]**Mail actions:**[ respond to this message ] [ mail a new topic ]

Bill,

I like the backward slices formalism, but don't quite see how this

handles the cannonical out-of-thin-air values example (the one where two

threads read/write x/y and return 42)? Is there a more developed version

I should wait for, or am I missing something here?

Sarita

*> -----Original Message-----
*

*> From: owner-javamemorymodel@cs.umd.edu
*

*> [mailto:owner-javamemorymodel@cs.umd.edu] On Behalf Of Bill Pugh
*

*> Sent: Friday, August 16, 2002 3:30 PM
*

*> To: javamemorymodel@cs.umd.edu
*

*> Subject: JavaMemoryModel: Our latest trial balloon
*

*>
*

*>
*

*>
*

*> 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
*

*>
*

-------------------------------

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

**Next message:**David Holmes: "RE: JavaMemoryModel: A simplified version of my model"**Previous message:**Sarita Adve: "JavaMemoryModel: A simplified version of my model"**In reply to:**Bill Pugh: "JavaMemoryModel: Our latest trial balloon"**Next in thread:**Bill Pugh: "RE: JavaMemoryModel: Our latest trial balloon"**Reply:**Bill Pugh: "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
*