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

[Peter Levart]

Hi Maurizio,


On 5/5/20 4:12 PM, Maurizio Cimadamore wrote:
>
> 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
>

There is one precondition which has to be present for this to work 
correctly. That close() is only executed by one thread. And in case of 
MemoryScope, this is true, because calls to close() are pre-screened by 
MemorySegment which checks that close() is executed only in owner thread.

So if this is true, then it follows that 'b' happens before 'c' because 
in 'b' we did not see the effect of 'c' and 'c' is volatile write and 
'b' is volatile read. So for the case that you was asking:

> One question: the more I look at the code, the less I'm sure that a 
> close vs. access race cannot occur. I'm considering this situation:
>
> * thread 1 does acquire, and find state == OPEN
> * thread 2 does close, set state to CLOSING, then checks if the adders 
> match
>
> But, how can we be sure that the value we get back from the adder 
> (e.g. acquires.sum()) is accurate and reflects the fact that thread 
> (1) has entered already?
>
...this is all that needs to be proven. For other cases, the proof of 
correctness is of course different.

So you are concerned about the case where the acquiring thread reads 
CLOSED. This is simple, since at that point the thread would just 
increment the releases (to level them back with acquires) and fail with 
exception. If that happens than we are also sure that the closing thread 
did successfully close the scope, so we have this mutual exclusion 
covered in this case where one thread is guaranteed to succeed while the 
other is guaranteed to fail.

The interesting case is when the acquiring thread reads CLOSING. In that 
case it will spin-loop, re-reading the state until it either gets reset 
back to OPEN or set to CLOSED. So we have 2 sub-cases how the loop ends:

- it finally reads CLOSED - in this case the closing thread decided to 
successfully close the scope, so acquiring thread fails

- if finally reads OPEN - in this case the closing thread decided that 
it should not close the scope so close() fails, but acquiring thread 
succeeds.

So in both above sub-cases we have the mutual exclusion covered.

Notice that for this last three cases it was not important what closing 
thread read from acquires.sum() and releases.sum(). So we don't have to 
prove anything about the ordering of those two operations.


Regards, Peter