Optimal Liveness-Enforcing Control for a Class of Petri Nets Arising in Multithreaded Software

We investigate the synthesis of optimal liveness-enforcing control policies for Gadara nets, a special class of Petri nets that arises in the modeling of the execution of multithreaded computer programs for the purpose of deadlock avoidance. We consider maximal permissiveness as the notion of optimality. Deadlock-freeness of a multithreaded program corresponds to liveness of its Gadara net model. We present a new control synthesis algorithm for liveness enforcement of Gadara nets that need not be ordinary. The algorithm employs structural analysis of the net and synthesizes monitor places to prevent the formation of a special class of siphons, termed resource-induced deadly-marked siphons. The algorithm also accounts for uncontrollable transitions in the net in a minimally restrictive manner. The algorithm is generally an iterative process and converges in a finite number of iterations. It exploits a covering of the unsafe states that is updated at each iteration. The proposed algorithm is shown to be correct and maximally permissive with respect to the goal of liveness enforcement.