RFR 8243491: Implementation of Foreign-Memory Access API (Second Incubator)

[Maurizio Cimadamore]

On 02/05/2020 09:45, Peter Levart wrote:
>
> Thread 1 does:
>
> a) increments 'acquires'
>
> b) reads OPEN from 'state'
>
>
> Thread 2 does:
>
> c) writes CLOSING to 'state'
>
> d) sums 'acquires'
>
>
> 'a' happens before 'b' happens before 'c' happens before 'd' => 'a' 
> happens before 'd'
>
Where did you get the "b" happens before "c" edge? I think it's more 
subtle then that? E.g. if thread 1 saw OPEN, _then_ you can establish an 
HB edge between (b) and (c). But it could also be the case that Thread 1 
reads CLOSED and starts to spin - so we need also to prove that there's 
some HB edges in that case (which I've tried to do in my email). I think 
this is the actual _difficult_ case to prove (I agree that the other is 
just transitive property of HB) - I think I've convinced myself that we 
should be in the clear also for the path when Thread 1 reads CLOSING, 
but I found it more subtle there to prove that either one thread or the 
other would fail.

E.g. can there be a situation where BOTH operations fail?

Maurizio