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 - http://www.cs.umd.edu/~pugh/java/memoryModel
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:41 EDT