We think we were able to relax things in a way that should satisfy the
concerns people raised.
An execution E contains a set of GC events. Assume the existence of a
particular set of sufficient synchronization edge for E (this contains
release/acquire pairs <r,a>). For each GC event g_i, there is a
partition of all actions into actions that come before g_i and actions
that come after g_i. If r is a read that sees a write w and r comes
before g_i, then w must come before g_i. If <r,a> is contained in the
set of sufficient synchronization edges and a comes before g_i, then r
must come before g_i.
These partitionings do not have to be otherwise consistent. For
example, you could have
an action x that comes before g1 and after g2
an action y that comes before g2 and after g1
At each GC event g_i, we can decide which objects are reachable,
unreachable and finalizable. Any decision consistent with the rules
below is acceptable.
If an object X is finalizable at g_i, then
* X must be unreachable at g_i,
* X must not have been previously finalizable,
* actions that happen-after the finalizer invocation
must come after g_i
An object X is unreachable at g_i if
* all reads that come after g_i that see a reference to X must see
writes to elements of objects that were unreachable at g_i, or see
writes that came after g_i.
* all active uses of X in thread T that come after g_i must occur as a
result of thread T performing a read that comes after g_i of a reference
to X or in the finalizer invocation for X.
A use of X is active if
it reads or writes an element of X
it synchronizes on X
it writes a reference to X
it is an active use of an object Y, and X is reachable from Y
X is reachable from a static field of a class loaded by a
An object B is reachable from A at g_i
if and only if
there is a write w1 to an element v of A that
is a reference to B
and there does not exist a write w2 to v
s.t. not (w2 \hb w1), and both w1 and w2
come before g_i
or there is an object C such that C is reachable from A
and B is reachable from C
Completion of a constructor of an object X is treated as a volatile
write to a hidden field of X that is read by the finalizer of X.
Bill and Jeremy
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:01:06 EDT