Re: JavaMemoryModel: The property of "race-free implies SC"

From: Bill Pugh (pugh@cs.umd.edu)
Date: Fri Oct 31 2003 - 12:57:01 EST


Slightly out of order:

At 2:53 PM -0700 10/30/03, Yue Yang wrote:
>On Wed, 29 Oct 2003, Bill Pugh wrote:
> > >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.
>>
>
>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?

Remember, "race-free (under SC) implies SC" and non-intuisive reads
are not part of the definition of the memory mode, but simply
desirable properties of a memory model.

Thus, we conclude that it is desirable to have a memory model such
that r1=r2=1 is illegal for the code fragment above.

Separately, we can show that the under the proposed JMM, r1=r2=1 is
illegal for the code fragment above.

At 2:53 PM -0700 10/30/03, Yue Yang wrote:
> > "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?

Because we want to specify a simple property, desirable in a JMM,
that can be stated and understood, without having to understand the
complexities or peculiarities of any particular JMM proposal. For
example, this way we know that when Sarita and when we talk about
about "Race free under SC implies SC", we know we are talking about
the same property, not two different properties.

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:52 EDT