[concurrency-interest] Relativity of guarantees provided by volatile

Marko Topolnik mtopolnik at inge-mark.hr
Thu Aug 23 05:19:06 EDT 2012


On 23. kol. 2012., at 10:01, Andreas Lochbihler wrote:
> Dear Marko,
> 
> On 23.08.2012 08:02, Marko Topolnik wrote:
>> This would be the situation you describe:
>> 
>>                                 /-->  Rrt6 --/->  Rrt9 -->  Rv0
>>     ---------------------------+------------+--------/
>>   /                            |     ------/
>> Wv0 --->  Rwt3 ->  Wv1 -->  Rwt6  |    /
>>         /                /   --|   /
>>        |                | /       /
>>        T3 ------------>  T6 ---->  T9
>> 
>> 
>> Notice I've fixed the naming somewhat.
>> 
>> T3, T6, T9 -- writes to currentTime
>> Rwt0, Rwt1 -- reads of currentTime by writing thread
>> Rrt1, Rrt2 -- reads of currentTime by reading thread
>> Wv0, Wv1   -- writes to the sharedVar
>> Rv0        -- read of the sharedVar
>> 
>> initially t = 0 ms;
>> T3 writes t = 3 ms;
>> T6 writes t = 6 ms;
>> T9 writes t = 9 ms.
>> 
>> The program outputs
>> 
>> Writing 0 at t = 0 ms
>> Writing 1 at t = 3 ms
>> Reading 0 at t = 9 ms
> 
> The JMM does not allow this output if sharedVar and currentTime are volatile, as the following reasoning shows: All actions in your example are synchronisation actions, i.e., they must be totally ordered by the synchronisation order, but there is none.
> 
> Assume for the sake of contradiction there was such a synchronisation order <so.
> 1. Wv0 <so Wv1 and Wv1 <so Rwt6 and Rrt9 <so Rv0 hold, because synchronisation order is consistent with program order.
> 2. Not T9 <so Rwt6, because otherwise, T9 would be an intervening write between T6 and Rwt6 since T6 <so T9 which contradicts well-formedness (JLS 17.4.7.5).
> 3. Hence Rwt6 <so T9 by totality of the synchronisation order.
> 4. T9 <so Rwt9, because Rwt9 sees T9, i.e., well-formedness forbids T9 <so Rwt9, and <so is total.
> 5. Wv1 <so Rwt9 by transitivity of 1., 3., 4.
> 6. Hence, Wv1 is an intervening write between Wv0 and Rv0 in the synchronisation order (since Wv0 <so Wv1 from 1.), which contradicts well-formedness (JLS 17.4.7.5).
> 
> Andreas

You are right, my example disregards the constraints imposed by the total synchronization order.

-Marko





More information about the Concurrency-interest mailing list