[concurrency-interest] Relativity of guarantees provided by volatile

Andreas Lochbihler andreas.lochbihler at kit.edu
Thu Aug 23 04:01:12 EDT 2012


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

-- 
Karlsruher Institut für Technologie
IPD Snelting

Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Am Fasanengarten 5, Geb. 50.34, Raum 025
76131 Karlsruhe

Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at kit.edu
http://pp.info.uni-karlsruhe.de
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum 
in der Helmholtz-Gemeinschaft


More information about the Concurrency-interest mailing list