At 4:48 PM -0600 10/23/03, Yue Yang wrote:
>One high level property of the proposed JMM is that if a program
>is free of race conditions (under Sequential Consistency
>interleaving), it should behave as SC.
>
>While this property seems to be a good standard for straight-line code,
>it is not as "natural" when applied for making branch decisions.
>Consider the following example:
>
>(initially a = b = c = 0):
>
>T1 T2
>
>r1 = a; r2 = b;
>c = 1; if(r2 > 0)
>if(r1 > 0) a = 1;
> b = 1;
>
>Because it's race-free under SC, it prohibits r1=r2=1 since SC doesn't
>allow it. Suppose we add a read of c in T2 as follows:
>
>r1 = a; r2 = b;
>c = 1; r3 = c;
>if(r1 > 0) if(r2 > 0)
> b = 1; a = 1;
>
>Now the code contains races and it doesn't need to follow SC.
"Race-free implies SC" is not part of the specification of the JMM.
Rather, it is a property that we have decided is desirable, and that
we can prove the JMM has.
The JMM has other properties as well. One of the properties Sarita
and I recently agreed should be a property of the JMM is the
non-intrusive reads property set out by Gao and Sarkar in "Location
Consistency -- A new Memory Model and Cache Consistency Protocol". It
states that adding additional reads to a program (where the values of
those reads are ignored) shouldn't have any effect on the program.
Now, actually, the semantics for final fields doesn't have this
property, because it might change a program in a way that allows an
object to be seen by other threads before the final fields of that
object are written. However, for the core memory model (excluding
final fields), both the model Jeremy and I have, and Sarita's current
proposal, have this property.
Similarly, if the threads can be partitioned such that no variables
are shared between partitions, a data race in one partition doesn't
effect the semantics of another partition.
>One alternative is to give up the "race-free implies SC" property.
Nope. Not going to happen. We are way too far along to reconsider
such basic changes.
But the major benefit of "race-free implies SC" is not that you know
race-free programs are SC. As you state, few programs actually are
data race free. Rather, it pushes your MM in a direction such that
your MM has other desirable properties for programs that are mostly
data race free.
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:52 EDT