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

From: Bill Pugh (pugh@cs.umd.edu)
Date: Thu Apr 22 2004 - 13:35:00 EDT


OK, here is a more refined attempt at finalization semantics.

For the moment, we have written it assuming a global ordering of
actions into finalization epochs. We are unsure if there are
potential problems associated with parallel garbage collectors.
Even with parallel garbage collectors, having semantics that say
finalization is performed in epochs may not be a problem.

We might be able to devise an appropriate technique that
only needs a partial order. But first, lets figure out
if this is acceptable, and then figure out whether any
changes need to be made to accommodate parallel GC.

---

All actions occur in one of a sequence of finalization epochs.

finalization epoch order is consistent with synchronization order and write \isSeenBy read order (in other words, if a read r sees the value of a write w, the write w cannot occur in a later finalization epoch than the read r).

After each finalization epoch, 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 the end of epoch i, then

* X must be unreachable at the end of epoch i,

* X must not have been previously finalizable,

* the actions that happen-after the finalizer invocation for X occur in epochs j > i

An object X is unreachable at the end of epoch i if and only if

* all reads in epoch j > i that see a reference to X must see writes to elements of objects that were unreachable at the end of epoch i, or see writes that occur after epoch i.

* all active uses of X in thread T in epoch j > i must occur as a result of thread T performing a read in some epoch j' such that j >= j' > 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 the end of epoch 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 occur in epochs no later than 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.

Jeremy and Bill

------------------------------- JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel



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