On Deadlocks in Concurrent Systems: A Petri Net based Deadlock Prediction and Avoidence''

We here provide a designer of an application in concurrent systems with a method for predicting and avoiding potential static deadlocks: --The method provides a guideline for transforming a set of two-phase locking (2PL) transactions, which are prone to deadlocks, into a set of deadlock free 2PL transactions without reducing potential concurrency unnecessarily.--It provides a guideline for transforming a parallel program into a deadlock free program without reducing potential concurrency unnecessarily.--It enables further the investigation ofpronenessto deadlocks of the following composition structures:boolean guarded commands, boolean and inputs guarded commands, andinput and output guarded commands. In further certifies concurrent applications to be free of deadlocks. The method is based on Petri net (PN) formal models of nested transactions and processes. The definition of PN models of nested transactions is based on different request models, namley an AND model, an OR model and an AND--OR model. A request model describes the conditions for statisfaction of requests of transactions. Generally in a resource allocation graph of a concurrent system, where transactions are in an AND request model, a cycle corresponds to a deadlock situation. Further in a resource allocation graph of a concurrent system, where transactions are in an AND--OR request model, a knot corresponds to a deadlock situation. Using PN feature, we here provide a unique structure which captures different conditions for the existence of deadlocks. It is a set of places which will remain empty, once it loses all tokens. The definition of PN models of processes in message passing is based on a subset of primitives of the CSP--language. One of the main reasons for the definition of the formal models based PN is the fact that PNs are appropriate for analyzing dynamic properties of systems, such as deadlocks, in combining static structures i.e. nets with marking. Further there exist software tools for their analysis and simulation. The act of deciding whether a designed application is prone to deadlock, is turned to decide whether the corresponding PN system is live. The defined PN models of concurrent systems do not belong to the class of free choice nets. We here give and prove a condition necessary and sufficient for the liveness of such nets.