Theodus/backpressure-model

possible deadlock?

sophiaIC opened this issue · 2 comments

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.

Configs-Backpressure-third.pdf

This isn't a valid trace as the blocker information wasn't used:

counter.pdf

This doesn't result in a deadlock