Proof techniques for distributed algorithms for deadlock handling

The authors consider deadlock handling in distributed systems in which processes may reside at different sites interconnected by a communication network. In particular attention is given to distributed deadlock handling in which no site has the knowledge of the global state of process dependencies. A review of two distributed algorithms for deadlock handling is presented with emphasis on the proof technique. It is shown that the distributed algorithms for deadlock detection can be classified based on the technique used for dissemination of dependency information, namely, top-down or bottom-up. The algorithms when presented without details of implementation mechanisms permit proofs of correctness which are simpler