possible deadlock?
sophiaIC opened this issue · 2 comments
sophiaIC commented
The attached example shows that it is possible for the algorithm to deadlock. It works by making Obstacle
cyclic -- cf the proof sketch for no deadlock in [Q22.] #(#8)
But it is possible that I have made an error, and the execution is not valid according to Theo's model.
lukecheeseman commented
This isn't a valid trace as the blocker information wasn't used:
lukecheeseman commented
This doesn't result in a deadlock