[concurrency-interest] check that volatile stores are not reordered with volatile loads

Oleksandr Otenko oleksandr.otenko at oracle.com
Tue Dec 2 10:50:24 EST 2014


The following proves volatile stores and loads form a total order.

Thread 1:
r1=y;
r2=x;

Thread 2:
r3=x;
r4=y;

Thread 3: x=1
Thread 4: y=1

You shall never observe (r1,r2,r3,r4) = (1,0,1,0)


You can build a similar proof for intra-thread reordering:

Thread 1:
y=1;
r1=x;
z=1;

Thread 2:
r3=z;
x=1;
r2=y;

You shall never observe (r1,r2)=(0,0)
You shall never observe (r1,r3)=(1,1)


Alex


On 02/12/2014 03:09, DT wrote:
> Folks,
> How can we check/prove (use case) that java guarantees that volatile 
> stores are not reordered with volatile loads?
> Any points to the code will be grateful.
>
> Thanks,
> Dmitry
>
> _______________________________________________
> Concurrency-interest mailing list
> Concurrency-interest at cs.oswego.edu
> http://cs.oswego.edu/mailman/listinfo/concurrency-interest



More information about the Concurrency-interest mailing list