Formal Verification of Distributed Deadlock Detection Algorithm Using a Time-dependent Proof Technique

A large number of published distributed deadlock detection/resolution algorithms are found to be incorrect because they have used informal approaches to prove the correctness of their algorithms. In this paper, we present a formal approach for the correctness proof and give an example of the proof. In this proposed approach, a formal model of distributed deadlock is presented with a local-time deadlock specification for correctness verification. With the formal model, we have an insight into the definition of deadlock in local views which is used to show the existence of a real deadlock. A rigorous proof to show the equivalence of local-time and global-time deadlock specifications is presented. Department of Computer Science University of Missouri-Rolla Rolla, Missouri 1 Introduction A distributed system consists of a set of processors connected by bidirectional communication links with processes and resources resident on each processor. Processes and resources communicate with each..