JavaMemoryModel: Definition of volatile revisited

From: Vijay Saraswat (
Date: Mon Mar 22 2004 - 08:59:51 EST

Folks --

I was working through some theorems on volatiles and noticed the following issue.

Is the following program properly synchronized (i.e. has no race conditions under SC executions)?

Initially: x=0, x volatile

Thread 1

Thread 2
Observatiom: r1=1,r2=2,r3=1

Weak semantics: Yes.
Strong semantics: Agrees with weak

No SC execution can produce this observation. So the x=1 in Thread 1 and x=2 in Thread 2 must be seen as conflicting pairs of writes (creating a race condition), even though they are writes to a volatile variable.

I believe this is not desirable.

Let us define two variants: a Write Total Read Weak (WTRW) and a Write Total Read Strong (WTRS) semantics. They are the same as weak and strong semantics respectively except that all write operations to the same location need to be totally ordered in the HB relation. Thus the notion of "last write" makes sense; a read always returns the value of the last write that HB the read (this is not a new condition, just follows from the standard notion of write visibility at a read).

WTRW semantics: Observation is not possible. (The two writes must be ordered wrt each other.)
WTRS semantics: Same as WTRW

With WT semantics, operations on volatile variables can never cause race conditions. I believe this is the desired behavior for volatile variables.

So it seems to me that we need a total order on writes to volatile variables. Hasnt this been discussed before? Why the change to the current language then?

JavaMemoryModel mailing list -

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