On Apr 30, 2004, at 2:44 AM, Sylvia Else wrote:
> At 05:00 PM 29/04/2004 -0400, Jeremy Manson wrote:
>
>> http://www.cs.umd.edu/~pugh/java/memoryModel/unifiedProposal/
>> model3.pdf
>
>
> Consider
>
> class Test {
> volatile int x;
>
> static void main(String args[]) {
> new Test().x = 1;
> }
>
> public void finalize() {
> int r = x;
> }
> }
>
> Behaviour in question: r = 0.
>
> I'm using a _so_ b to mean a is before b in the synchronization order.
>
> For this to occur, we require for some reachability decision point d,
>
> r = x _so_ x = 1 [that is to say, not (x = 1 _ so_ r = x)]
> x = 1 comes before d.
> r = x comes after d.
>
> Since by hypothesis r =x _so_ x = 1, there is no release acquire pair.
> The only accesses of the object other than its initialization and x =
> 1 are in the finalizer.
> The object is never definitely reachable.
>
> Seems to me that the finalizer model is satisfied by this behaviour.
>
> What have I missed?
>
We can't mark the object as unreachable at a d that comes before
the write x = 1, since that is an active use that doesn't result
from the finalizer invocation.
So x = 1 must come before d.
The read r = x happens-after the finalizer invocation, so
the read r = x must come-after d.
We added an additional rule:
> If $x$ and $y$ are synchronization actions on the same variable or
> monitor, $x$ comes-before $d_i$ and $y$ comes-after $d_i$, then
> $x$ comes-before $y$ in synchronization order.
Since x = 1 comes-before d and r = x comes-after d,
they must also have that ordering in the synchronization order.
Thus, r = 0 is impossible.
Now, in this case, x is volatile.
We discussed whether we want to forbid r = 0 for the non-volatile
case. At least, we were leaning towards forbidding r = 0, but
then we shifting towards allowing it. The current spec allows
r = 0 if x is non-volatile.
I don't remember any strong justification for this either way.
The guarantees you get from forbidding r = 0 are so weak that
it is difficult to use them to build correct finalization built
on it.
On the other hand, it is hard to imagine compiler or processor
optimizations that could result in r = 0.
If we did want to forbid r = 0, we could add:
> If an object $X$ is marked as unreachable at $d_i$,
> and there are two conflicting writes $w_1$ and $w_2$ to a field
> or element of $X$,both $w_1$ and $w_2$ come-before $d_i$,
> and $w_1 \hb w_2$, then no read that comes-after $d_i$
> sees the write $w_1$.
Thoughts?
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:06 EDT