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
x=1
Thread 2
x=2
r1=x
r2=x
r3=x
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?
Best,
Vijay
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:01:01 EDT