RE: JavaMemoryModel: Our latest trial balloon

From: Sarita Adve (sadve@cs.uiuc.edu)
Date: Wed Aug 21 2002 - 11:42:40 EDT


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



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