JavaMemoryModel: Another attempt at formalizing finalization; need particular attention from parallel GC people

From: Jeremy Manson (jmanson@cs.umd.edu)
Date: Fri Apr 23 2004 - 16:13:12 EDT


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
                reachable classloader

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