Bill & Jeremy -
I like the idea, but I'm not sure I understand all the implications of this.
You are forcing the epoch order to be consistent with two other orders:
1) The synchronization order (a total order), and
2) The is-seen-by order.
I guess these are technically consistent, since they mostly order different
actions. But I think they're not consistent in an intuitive sense.
Consider:
Thread 1: Thread2:
... = y; synchronized(lock2) {}
synchronized (lock1) {} y = null;
Assume the acquisition and release of lock1 precede those of lock2
in synchronization order, but the read of y sees the write,
because a really clever optimizer decided that null was a possible value for
y. (Since the locks are not the same, there is no happens-before edge,
so I think this is OK.)
How do you model the case in which the GC happens between the release
of lock1 and the acquisition of lock2? Presumably the write to y
goes into the preceding epoch. But now reachability in the model at
the end of the previous epoch doesn't correspond to what a GC would
actually observe. At this point my intuition fails me completely.
Are we indirectly imposing constraints on the is-seen-by order for
finalizer-free code?
Other concerns (which may also be OK):
- It would be nice to be more explicit about the rules for finalizer
execution and visibility. I think the rule that a nonvolatile write
to the object must be visible to the finalizer no longer appears.
(In my opinion, no great loss, but ...). It's probably also worth
stating explicitly that if an object becomes finalizable in epoch i,
then the finalization actions must appear in some epoch > i (or not
at all, e.g. because earlier finalizers failed to terminate).
- The current rules state that if I have two objects A and B each
pointing to the other, they are both reachable if either
1) I definitely assign A to x, or
2) I definitely assign B to y
But if there is a race, and I may do one or the other depending on the
outcome of the race, than they may both be finalized prematurely.
That's a little weird, but I can certainly live with it.
- "element of X" presumably means field or array element?
- "writes a reference to X" includes writes to locals? Otherwise isn't
this a write to an element of an object, from which X is then reachable?
Hans
> -----Original Message-----
> From: owner-javamemorymodel@cs.umd.edu
> [mailto:owner-javamemorymodel@cs.umd.edu]On Behalf Of Bill Pugh
> Sent: Thursday, April 22, 2004 10:35 AM
> To: javamemorymodel-cs.umd.edu
> Subject: JavaMemoryModel: Another attempt at formalizing finalization;
> need particular attention from parallel GC people
>
>
> 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
-------------------------------
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