There is no data race because there are no data accesses, so the example is
correctly synchronized and must be SC. r1=v is ordered before v=1 by synch
order as you point out. So by the synchronization consistency condition (#5)
of the well-formed execution clause, r1=v can't see the value of v=1. (I
notice that other parts of that condition are not as well specified as they
could be, we'll fix that.) Let me know if I misinterpreted your question.
> -----Original Message-----
> From: firstname.lastname@example.org
> [mailto:email@example.com] On Behalf Of Sylvia Else
> Sent: Thursday, April 15, 2004 2:00 PM
> To: JavaMemoryModel@cs.umd.edu
> Subject: JavaMemoryModel: Non SC behaviour using volatiles.
> I think I've seen comments here that assume that code that
> manipulates only
> volatiles must be correctly synchronized, and would therefore be SC.
> volatile v, w, initially 0
> Thread 1
> r1 = v;
> r2 = w;
> Thread 2
> w = 2;
> v = 1;
> Behaviour in question, r1 = 1, r2 = 0
> Since r2 = 0, there cannot be a happens-before edge from w =
> 2 to r2 = w,
> therefore r2 = w is ordered before w = 2 in the
> synchronization order. r1 =
> v must be ordered before r2 = w in the synchronization order because
> program order must be respected for the thread. Ditto w =2 is ordered
> before v = 1. So r1 = v must be ordered before v = 1.
> However, there is no happens-before edge from r1 = v to v =1,
> so there is
> nothing to stop r1 = v from seeing the write v =1.
> At the moment, it seems to me that behaviour in question is
> permitted, even
> though it is not SC.
> This program contains data races, so is not correctly
> synchronized and is
> not required to be SC.
> JavaMemoryModel mailing list -
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:01:04 EDT