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
