Finalization "interaction with memory model" (12.6.2)

[Alex Buckley]

The JSR 133 spec available from jcp.org as Proposed Final Draft 2 is 
fractionally clearer than JLS 12.6.2 because of a comma before the "both 
w1 and w2" clause:

-----
An object B is definitely reachable from A at di if there is a write w1 
to an element v of A such that the value written by w1 is a reference to 
B and there does not exist a write w2 to v s.t. ¬(w2 ==hb==> w1), and 
both w1 and w2 come-before di.
-----

(The PFD2 document is dated May 28, 2004; I have a version dated August 
24, 2004 with slightly different section numbering, though the text 
above is identical. I do not remember where I obtained it from.)

The proposal below is an improvement because of its "might overwrite" 
narration, but the treatment of (the non-existent) w2 is still 
confusing. If I was spending time on it, I would try very hard to find 
an hb(...) clause that is true rather than false. However, 12.6.2 is 
slated for removal when finalization is removed, so it's not a priority.

Alex

On 5/2/2022 4:25 PM, Hans Boehm wrote:
> It seems like once a year or so, I try to decode
> https://docs.oracle.com/javase/specs/jls/se18/html/jls-12.html#jls-12.6.2
> 
> There seem to be two particularly confusing consecutive paragraphs here, in
> a confusing section. I always seem to get stuck here. Arbitrarily picking
> on the second one:
> 
> An object B is definitely reachable from A at di if there is a write w1 to
> an element v of A such that the value written by w1 is a reference to B and
> there does not exist a write w2 to v such that hb(w2, w1) is not true and
> both w1 and w2 come-before di.
> 
> I always have trouble parsing this. I think it's because the syntactic
> position of "both w1 and w2 come-before di" suggests it's a constraint on
> w2 (which must not exist), but in fact half of it is a constraint on w1,
> which must exist. I don't think we normally mix up mathematical constraints
> this way.
> 
> Could we possibly rephrase this as something like:
> 
> An object B is definitely reachable from A at di if:
> a) There is a write w1 to an element v of A such that the value written by
> w1 is a reference to B, and w1 comes-before di.
> b) There does not exist a write that might overwrite w1 before di. That is,
> there does not exist a write w2 to v such that hb(w2, w1) is false and w2
> also comes-before di.
> 
> ?
> 
> This is unfortunately longer. But I think the intended meaning is the same.
> And my current feeling is that I might still be able to parse this next
> year, without having to again spend time decoding it.
> 
> I think the preceding paragraph could use essentially the same treatment.
> 
> Hans