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
