Thanks for your comments.
People have asked me to post to the list how CCM semantics handles this
case, so here goes. The answer per CCM semantics is Yes.
The constraints produced are (simplified action sets):
Ai = Bi = Yi = 0
R1 = A1r
R1 == 0 --> Y1w=1,
R1 != 0 --> B1w=1
R2 = Y2r,
R3 = B2r,
R2+R3 != 0 -> A2w = 1
The linking in question is:
Y2r = (R1 == 0)? Y1w : Yi
B2r = (R1 != 0)? B1w:Bi
A1r = (R2+R3!=0)?A2w:Ai
The constraints can be simplified to:
R2 = (R1==0)? 1:0
R3 = (R1!=0)? 1:0
R1=(R2+R3 !=0)?1:0
This has the unique solution
R1=R3=1, R2=0
From an operational viewpoint, given the linking one can
unconditionally establish that R2+R3 != 0 since one of the branches must
be taken by the first thread. But this is enough to discharge the
conditional in the second branch and propagate 1 for R1. This forces R2
to be 0 and R3 to be 1.
Best,
Vijay
Bill Pugh wrote:
> My first reaction to this test case is that the behavior in question
> is neither something that must be prohibited nor something that must
> be allowed.
>
> I don't see any reasonable optimizations that would result in this
> behavior, nor do I see any immediate problems with allowing this.
>
> Bill
>
>
>
> On Mar 8, 2004, at 8:29 PM, Vijay Saraswat wrote:
>
>>
>>
>> ----------------------------------------------------------
>> Test 14a
>> Initially: a=b=y=0
>>
>> Thread 1
>> r1 =a
>> if (r1 == 0)
>> y =1
>> else
>> b =1
>>
>> Thread 2
>> r2=y
>> r3=b
>> if (r2+r3 !=0)
>> a=1
>>
>> Question: r1=r3=1, r2=0?
>> ---------------------------------------------------------------
>
>
> -------------------------------
> JavaMemoryModel mailing list -
> http://www.cs.umd.edu/~pugh/java/memoryModel
>
>
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:59 EDT