Re: JavaMemoryModel: Are the volatile semantics strong enough?

From: Bill Pugh (pugh@cs.umd.edu)
Date: Fri Aug 01 2003 - 13:13:07 EDT


We have a general rule that:
  * correctly synchronized programs exhibit only SC behaviors

Now, I think we need to classify any program using only volatile variables
as correctly synchronized.

Which means that programs that use only volatile variables exhibit
only SC behaviors.

I think, as Jan-Willem suggestions, that the way to solve this is to
say that there is a total order over all synchronization actions that
is consistent with program order. This total order is used to
determine when there is an inter-thread hb edge induced from
synchronization actions and which value is seen by volatile reads.
The synchronization order will be consistent with hb order, but need
not be consistent with the causal order.

Volatile example 1:
v = w = 0; v and w are volatile

>v=1 w=1 r1=v r3=w
> r2=w r4=v
>
>Can r1 == r3 == 1, but r2 == r4 == 0?

Not allowed, since there is no synchronization order that allows this.

Volatile example 2:
>Initially, x = v = w = 0; v and w are volatile
>
>x=8 w=2 r1=v
>v=1 x=9 r2=x
> r3=w
>
>Can r1==1, r3==0 but r2==9?

Synchronization order:

x = 8
v = 1
                 r1 = v
                 r2 = x
                 r3 = w
          w = 2
          x = 9

So r1 = 1 and r3 = 0. But there is no happens before edge between r2
= x and x = 9, so r2 may be either 8 or 9 (but not 0).

Note: we could try to weaken this to say that there is only a total
order over volatile operations but not locks. However, I don't think
this difference would be detectable.

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



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