**Next message:**Sarita Adve: "JavaMemoryModel: A simplified version of my model"**Previous message:**Bill Pugh: "RE: JavaMemoryModel: Comments on Sarita's example for our model, and on Sarita's model"**In reply to:**Bill Pugh: "RE: JavaMemoryModel: Comments on Sarita's example for our model, and on Sarita's model"**Messages sorted by:**[ date ] [ thread ] [ subject ] [ author ]**Mail actions:**[ respond to this message ] [ mail a new topic ]

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

**Next message:**Sarita Adve: "JavaMemoryModel: A simplified version of my model"**Previous message:**Bill Pugh: "RE: JavaMemoryModel: Comments on Sarita's example for our model, and on Sarita's model"**In reply to:**Bill Pugh: "RE: JavaMemoryModel: Comments on Sarita's example for our model, and on Sarita's model"**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
*