On Wed, 29 Oct 2003, Bill Pugh wrote:
> 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.
>
So why do we need to define "race-free" using SC, while SC is not the
underlying memory model?
> 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.
>
If we combine the two properties -- "race-free (under SC) programs
are SC" and "non-intrusive reads", we have to conculde that r1=r2=1 is
also illegal for the 2nd case, right?
I feel the usage of a discrepent memory model for defining the desired
property might be a source for a lot of subtleties like this, which is
fine if there is a good reason for doing so. Otherwise, I'm afraid it'll
unnecessarily make the JMM design more complicated since you have to
consider all these implications.
- Jason
-------------------------------
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