Efficient Distributed Deadlock Avoidance with Liveness Guarantees

Abstract

We present a deadlock avoidance algorithm for distributed systems that guarantees liveness. Deadlock avoidance in distributed systems is a hard problem and general solutions 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 perform safe resource allocation based on local data only, that is, no communication between components is required. While avoiding deadlock, those protocols, however, did not avoid starvation: they guaranteed that some process could always make progress, but did not guarantee that every individual process would always eventually terminate. In this paper we present a resource allocation mechanism that avoids deadlock and guarantees absence of starvation, without undue loss of concurrency. The only assumption we make is that the local scheduler is fair. We prove the correctness of the algorithm and show how it can be implemented efficiently.

Type
Publication
Proc. of the 6th ACM & IEEE Conference on Embedded Software (EMSOFT'06), pp12-20. ACM Press, 2006
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.