This problem is a very close sibling of the problem I cited in a
previous message for Bill's model and mine, and has a similar solution.
At that time, I referred to the solution informally as using path
information/correct state, but Bill's use of the term "backward slice"
is nicer.
So more formally, I need to add that (1) when generating P-R, replace R
with a register assignment *only when the backward slice of R is the
same in the original and new execution*, and (2) a data race in one
execution is said to occur in another *only when the backward slices for
the memory accesses in the race are the same in both executions*. The
updated model is at http://www.cs.uiuc.edu/~sadve/jmm.pdf. The term
"backward slices" still needs to be nailed down more precisely.
While fixing the above, I figured another way to further simplify my
model. That's in the next message.
Sarita
> -----Original Message-----
> From: Bill Pugh [mailto:pugh@cs.umd.edu]
> Sent: Friday, August 16, 2002 3:28 PM
> To: Sarita Adve; javamemorymodel@cs.umd.edu
> Subject: RE: JavaMemoryModel: Comments on Sarita's example
> for our model, and on Sarita's model
>
>
> At 12:46 PM -0500 8/16/02, Sarita Adve wrote:
> >
> >
> >>
> >> 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.
> >
> >This isn't the case if you consider that the program is also
> a function
> >of the initial conditions, command line, etc. That is, the
> program with
> >initial condition foobar = true is different from the program with
> >foobar = false.
>
>
> No, different initial conditions do not make it a different program.
> Consider:
>
>
>
> Initially, x = y = 0, foo = false and bar = false
>
>
> Thread 1:
> if foo
> x = 1
> y = 1
> bar = true
>
> Thread 2:
> if x = 1
> y = 1
>
> Thread 3:
> if y = 1
> x = 1
>
>
> Thread 4:
> foo = true
>
> Now, I claim that bar = false, x = 1 and y = 1 should be an illegal
> result.
>
> Different initial conditions can be (and typically are) the result of
> a prefix of the program producing different results.
>
>
>
-------------------------------
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