Re: JavaMemoryModel: New approach to defining the Java Memory Model

From: Yue Yang (
Date: Wed Aug 07 2002 - 19:45:58 EDT

The bypassing table I just proposed would still have some barrier effect
for redundant locks in that the previous Read can be blocked by a later
Unlock and a later Write can be blocked by a previous Lock as follows:

r1 = a;
Lock l1;
Unlock l2;
b = 1;

So to eliminate the barrier restriction in the bypassing table, I need to
allow reordering across synchronization boundary and then filter out the
illegal results from condition legalNormalWrite.

For example, if we set R->U and R->WV to "yes", the additional condition
for legalNormalWrite(r, w) is:

"If there exists an Unlock or a WriteVolatile instruction u from the same
thread of r that has bypassed the Read instruction r, then
synchronized(u,w) must be false."

or formally, conjunct the following to legalNormalWrite(r, w):

( (exists u in GIB, s.t. (op(u) = Unlock or op(u) = WriteVolatile) and
t(u) = t(r) and pc(u) > pc(r))
synchronized(w, u) = false )

Whether this is "elegant" for capturing the general case is subject to
comparison with alternative solutions. But our approach provides a clear
and straightforward executable encoding for JMM that facilites
verification. Hence, it can be applied as a useful tool.

-- Jason

JavaMemoryModel mailing list -

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