Symbolic Computation and Representation of Deadlock Avoidance Policies for Complex Resource Allocation Systems with Application to Multithreaded Software

In our recent work, we proposed a series of binary decision diagram (BDD-) based approaches for developing the maximally permissive deadlock avoidance policy (DAP) for a class of complex resource allocation systems (RAS). In this paper, (i) we extend these approaches by introducing a procedure that generates a set of comprehensible "guard" predicates to represent the resulting DAP, and (ii) we customize them to the problem of deadlock avoidance in shared-memory multithreaded software, that has been previously addressed by the Gadara project. In the context of this last application, the generated guards can be instrumented directly into the source code of the underlying software threads, providing, thus, a very efficient and natural representation of the target policy. At the same time, by integrating the representational and computational strengths of symbolic computation, the presented approach can support the computation of the maximally permissive DAP for RAS corresponding to problem instances of even larger scale and complexity than those addressed in the current literature.