In this paper, we present a formal model of deadlock in a distributed system and develop the deadlock specification in terms of time-dependent predicates. Primitive activities of processes in the distributed system are specified by the predicates so that system behaviors can be described by logic operations. With the formal model, we have an insight into the definition of deadlock in local views. A rigorous proof to show the equivalence of local-time and global-time deadlock specifications is presented. The local-time deadlock specification, which defines the timing of dependence between deadlocked processes, will be useful in the correctness verification of distributed deadlock detection/resolution algorithms.
Li, Pei-yu and McMillin, Bruce M., "Formal Model and Specification of Deadlock" (1993). Computer Science Technical Reports. 52.
© 1993 University of Missouri--Rolla, All rights reserved.