Reachable State Spaces of Distributed Deadlock Avoidance Protocols
We present a family of efficient distributed deadlock avoidance algorithms with applications to distributed real-time and embedded systems (DREs), which subsumes previously known solutions as special instances. Then we use this family to study the reachable set of states and the allocation sequences allowed by the different protocols. This result enables a new proof method for showing freedom from deadlock of variations of deadlock avoidance protocols.
Distributed deadlock avoidance 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. The most basic algorithm \BasicP, performs only one operation per request using one counter per site. The protocol \LiveP, which also guarantees liveness globally, needs to performs a logarithmic number of operations per request, using a linear number of counters in each site (in terms of the total ammount of resources). The family of algorithms that we introduce here, called \kEfficientP, subsumes these as special cases. This family allows us to compare the protocols according to the set of reachable states and their legal allocation sequences. We prove that, even though the more liberal algorithms allow more concurrency, all algorithms can reach the same set of states. We capture this set of states as a network invariant.