Re: JavaMemoryModel: Another litmus test for strong vs. weak volatiles

From: Bill Pugh (pugh@cs.umd.edu)
Date: Thu Mar 25 2004 - 11:28:15 EST


On Mar 18, 2004, at 5:21 PM, David Holmes wrote:

>> Initially, x = y = v = 0, v is volatile
>>
>> Thread 1:
>> x = 1
>> v = 1
>>
>> Thread 2:
>> y = 1
>> v = 2
>>
>> Thread 3:
>> r1 = v
>> r2 = v
>>
>> Thread 4:
>> r3 = v
>> r4 = x
>>
>> ...
>> So is there a happens-before edge from x = 1 to r4 = x? There is under
>> the strong semantics, but not under the weak semantics.
>
> Does this boil down to whether the two statements in Thread 3 can be
> reordered?
>
> Otherwise "roach motel" rules say r4 == 1
>
> David Holmes
>

"Roach motel semantics" are only an approximation to the semantics of
synchronization
and volatiles.

Roach motel semantics guarantee that you can
* move non-volatile memory accesses into a synchronized block,
* reorder a non-volatile memory access and a following volatile read
* reorder a volatile write and a following non-volatile access

Roach motel semantics do _not_ say you may never reorder:
* a non-volatile memory access out of a synchronized block
* reorder a non-volatile memory access and a following volatile write
* reorder a volatile read and a following non-volatile access

You have to look deeper to figure out whether these reorderings are
possible.

In this example, since we have r1 = 1 and r2 = 2, we know
that in the global order over accesses to v, the write v = 1
occurred first.

Since r3 = v sees 2, and we know v = 1 occurred before v=2 we know that
this read occurs after both writes

Under the strong interpretation, this means that there is a
happens-before
edge from v=1 to r3=v. Under the weak interpretation, there is not.

        Bill

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



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