Java Memory Model mailing list archive: JavaMemoryModel: correc (original) (raw)

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