A Theory for Deadlocks

Abstract:

Deadlock detection is an elementary problem in computer science, yet
algorithms for detecting deadlocks over resources in a distributed
system are curiously prone to errors. This anomaly calls for a theory
that will help us understand existing algorithms and design new
algorithms. Surprisingly, most papers in the literature have either no
difinition of what a deadlock is, or a bad definition; this fact itself
accounts for many of the errors. The first task in developing a theory
is therefore to choose an appropriate definition for a deadlock. Since
this theory is to be used for the analysis and synthesis of detection
algorithms, it should focus on what an algorithm can observe (in this
sense, it is an $operational$ theory); accordingly, the definition
chosen here is in terms of locally observable facts, and does not use
real time. The theory begins with a rigorous formulation of the
interaction between processes and resources, and its development is via
logical deduction, rather than operational arguments. The results
examine the effect of aborting processes on deadlock detection, clarify
the difference between a process and a resource, and reveal the
structure of detection algorithms. To illustrate its application, the
theory is used to analyze several errors and algorithms in the
literature.