A Distributed Deadlock Resolution algorithm for the AND model

Previous proposals for Distributed Deadlock Detection/Resolution algorithms for the AND model have the main disadvantage of resolving false deadlocks, that is, nonexisting or currently being resolved deadlocks. This paper pro vides an algorithm free of false deadlock resolutions. A simple specificati on for a safe deadlock resolution algorithm is introduced, and the new dist ributed solution is developed in a hierarchical fashion from its abstract s pecification. The algorithm is probe-based, uses node priorities, and coord inates the actions of resolvers so that false deadlocks are not resolved. T he solution is formally proven correct by using the Input-Output Automata M odel. Finally, a study about the liveness of the algorithm is provided.