Deadlock-Avoidance Control of Multithreaded Software: An Efficient Siphon-based Algorithm for Gadara Petri Nets

This paper presents an efficient implementation of an iterative control algorithm for the synthesis of maximally-permissive liveness-enforcing control policies for Gadara nets presented in earlier work. Gadara nets are a special class of Petri nets arising when modeling multithreaded software for the purpose of deadlock analysis and resolution. The considered control synthesis algorithm is based on structural analysis of Gadara nets in terms of a certain type of siphons, called resource-induced deadly-marked siphons. We propose a new customized mixed integer programming formulation to detect these siphons in Gadara nets. We then compare the performance of our customized algorithm with that of a generic siphon detection algorithm for process-resource nets in the context of the iterative control algorithm. Finally, we investigate the scalability of the overall algorithm to large program models.