Proving the correctness of distributed deadlock detection algorithms (DDDAs) is difficult. Most previous works on DDDAs have either not provided a proof of correctness, provided only informal or intuitive arguments for correctness, or used simulations to verify correctness. In many cases, informal proofs or verifications by simulation have not been fail-safe and the algorithms have subsequently been found to be incorrect.

The emphasis in this paper is on providing a formal proof of correctness of distributed deadlock detection and resolution (DDDR). A class of algorithms, known as priority-based probe algorithms, for DDDR is investigated. In particular, the priority-based probe algorithm of Choudhary et al. [1] is shown to have flaws; the flaws are removed to obtain a modified algorithm, and the modified algorithm is proven correct. The proof technique involves abstracting the essential properties of an algorithm by invariants, which are necessary and sufficient conditions to be satisfied to detect all deadlocks and not report any false deadlocks. The authors claim that this work is the first attempt at a formal proof of a DDDA.