RE: JavaMemoryModel: Semantics musings

From: Bill Pugh (pugh@cs.umd.edu)
Date: Wed Sep 26 2001 - 16:52:43 EDT


At 9:03 AM -0400 9/26/01, Bowen Alpern (914) 945-3447 wrote:
>
> Bill
>
>Is there really more to add than "the values seen from a data race are
>unspecified"?
>
> Bowen

Yes, for a number of reasons.

Once we've determined that a program has data races, we know that it
isn't guaranteed to execute using sequentially consistent semantics.
So even defining the values "seen from a data race" is tricky,
because our previous definition won't include all of them (e.g.,
because certain program paths will never be explored if the program
is executed under sequentially consistent semantics).

Sarita has an attempt at this:
At 1:44 PM -0500 7/13/01, Sarita Adve wrote:
>You may want to see
>http://www.cs.uiuc.edu/~sadve/Publications/isca91.dataraces.ps.
>This paper from ISCA'91 describes a sequentially consistent semantics for
>all parts of a program that are not "affected" by a data race. The "affects"
>relation is in terms of happens-before. The paper gives hardware constraints
>to ensure the above as well.

however, in Sarita's paper, data race contamination quickly spreads
so that you can't say anything about the semantics of anything
influenced by a data race.

Even once you have identified them, you need to do more that state
that they are unspecified. For example, the values read need to be
type safe. Furthermore, the value read needs to be a value written
there previously, although "previously" is tricky to define in a
multithreaded context. For example, given:

Initially, x = y = 0

thread 1:
r1 = x
y = r1

thread 2:
r2 = y
x = r2

You don't want this fragment to result anything other than
x=y=r1=r2=0. You could argue that x=y=r1=r2=42 is legal, since it is
typesafe and each read is seeing the value of another write. But it
must not be legal.

You also want a little more, something to the effect of being able to
recover from data races. For example:

Initially, x = 0

Thread 1:
x = 1

Thread 2:
x = 2

Thread 3:
join thread 1 // use synchronization to wait for thread 1 to terminate
join thread 2 // use synchronization to wait for thread 2 to terminate
r1 = x
x = 3
r2 = x

You want this program to have the semantics that r1 is either 1 or 2
(but not 0), and r2 is 3.

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



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