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