On the deadlock analysis of multithreaded control software

The long interest in finding efficient solutions to deadlock occurrence induced by resource sharing is persistent in the context of concurrent control software production. Petri net-based correction techniques which were traditionally applied in the context of flexible manufacturing systems (FMS) constitute a promising new approach. In this vein, Gadara nets were introduced as an attempt to import the strengths of these techniques into the software domain. In this paper, we prove that these Petri nets are close to a subclass of S⁴PR (a widely-exploited class in the context of FMS) and provide some related equivalence results. Some limitations which Gadara nets present for the modelling and automated correction of software are also unveiled. Last but no least, we present formal proofs of the theorems characterising non-liveness in Gadara nets. To our knowledge, no such proofs were published before.