JavaMemoryModel: correct synchronization

From: Adam Welc (welc@cs.purdue.edu)
Date: Fri Feb 20 2004 - 17:16:08 EST


Hello,
I am trying to get a better understanding of what it means for a program
to be correctly synchronized (as defined in the JSR-133). The JSR states
that:

"A data race occurs in an execution of a program if there are conflicting
actions in that execution that are not ordered by synchronization (ie, by
a happnes-before relationship). A program is correctly synchronized iff
all sequentially consistent executions are free of data races"

Is the following program correctly synchronized?

      public static boolean w = false;
      public static boolean v = false;

   T1 T2
w=true; while(true) {
synchronized(M) { synchronized(M) {
 v =true; if (v) break;
} }
                         }
                         boolean tmp=w;

In any legal execution of that program the following sequence of actions
will occur: T1 writes to w, T1 releases M, T2 acquires M, T2 reads w. This
is enforced by the fact that the read of w can only happen after T1 exits
the loop, which in turn can only happen after T2 modifies v.

For example (arrow describes a happens-before edge):

T1 T2
              ACQ(M)
              READ(v) // v still false; cannot exit loop
              REL(M)
WRITE(w)
ACQ(M)
WRITE(v)
REL(M) ------->
              ACQ(M)
              READ(v) // exits the loop
              REL(M)
              READ(W)

Acording to the definition above, there is a happens-before relationship
(by transitivity) between the write to w and the read from w in any
execution of the program. But is it correctly synchronized?

Best regards

Adam Welc

-- 
Adam Welc
Computer Science Building, room 274
West Lafayette, IN 47906
Telephone number (work): (765) 4947836

http://www.cs.purdue.edu/homes/welc

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



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