INVARIANT-BASED VERIFICATION OF A DISTRIBUTED DEADLOCK DETECTION ALGORITHM

Most previous proposals for distributed deadlock detection are incorrect because they have used informal/intuitive arguments to prove the correctness of their algorithms. Informal and intuitive arguments are prone to errors because of the highly complex nature of distributed deadlock detection/resolution algorithms. In this paper we first correct the priority-based probe algorithm for distributed deadlock detection and resolution of Choudhary et al. [3] and then formally prove that the modified algorithm is correct (i,e., it does detect all deadlocks and does not report phantom deadlocks). Our proof technique is novel because we first abstract the properties of the deadlock detection and resolution algorithm by invariants, and then show that the invariants imply the desired correctness of the algorithm. This is the first attempt at a formal proof of the correctness of a distributed deadlock detection and resolution algorithm.