Finalization "interaction with memory model" (12.6.2)

[Hans Boehm]

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