A Family of Distributed Deadlock Avoidance Protocols and their Reachable State Spaces

Abstract

We study resource management in distributed systems. Incorrect handling of resources may lead to deadlocks, missed deadlines, priority inversions, and other forms of incorrect behavior or degraded performance. While in centralized systems deadlock avoidance is commonly used to ensure correct and efficient resource allocation, distributed deadlock avoidance is harder, and general solutions are considered impractical due to the high communication overhead. However, solutions that use only operations on local data exist if some static information about the possible sequences of remote invocations is known. We present a family of efficient distributed deadlock avoidance algorithms that subsumes previously known solutions as special instances. Even though different protocols within the family allow different levels of concurrency and consequently fewer or more executions, we prove that they all have the same set of reachable states, expressed by a global invariant. This result enables: 1. a design principle: the use of different protocols at different sites does not compromise deadlock avoidance; 2. a proof principle: any resource allocation protocol that preserves the global invariant and whose allocation decisions are at least as liberal as those of the least liberal in the family, guarantees absence of deadlock. We study how to generate efficient resource allocation controllers that implement distributed deadlock avoidance and are specific for a given application. We classify the solutions depending on the type and initial ammount of the resources handled. General solutions to deadlock avoidance in distributed systems are considered impractical due to the high communication overhead. In previous work, however, we showed that practical solutions exist when all possible sequences of resource requests are known a priori in the form of call graphs; in this case protocols can be constructed that involve no communication. These run-time protocols make use of annotations of the call-graph computed statically. If the annotations are acyclic, then deadlocks are unreachable. In this paper we first show that the algorithm that computes acyclic annotations is complete, in the sense that every optimal annotation can be generated. Second, we show that if the annotations are not acyclic, then checking whether deadlocks are reachable is NP-complete. Third, we study the problem of computing minimal annotations given constrainst in the system’s initial resources, and prove the complexity of this problem: if the restrictions are general the problem is NP-complete, while if the only restrictions are binary semaphores the problem becomes polynomial.

Publication
Fundamental Approaches to Software Engineering (FASE'07), vol. 4422 of LNCS, pp155-169. Springer, 2007
César Sánchez
César Sánchez
Research Professor

My research focuses on formal methods, in paricular logic, automata and game theory. Temporal logics for Hyperproperties. Applications to Blockchain.