Abstract
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.
Recommended Citation
Li, Pei-yu and McMillin, Bruce M., "Formal Model and Specification of Deadlock" (1993). Computer Science Technical Reports. 52.
https://scholarsmine.mst.edu/comsci_techreports/52
Department(s)
Computer Science
Report Number
CSC-93-31
Document Type
Technical Report
Document Version
Final Version
File Type
text
Language(s)
English
Rights
© 1993 University of Missouri--Rolla, All rights reserved.
Publication Date
August 1993
