A generalized deadlock predicate (Q1085972): Difference between revisions

Satisfiability of the deadlock predicate contructed by the semaphore invariant method is a necessary condition for total deadlock in PV programs. \textit{E. M. Clarke jun.} [ACM Trans. Program. Lang. Syst. 2, 338-358 (1980; Zbl 0468.68024)] has developed a technique, based on a view of resource invariants as fixed points of a functional, for constructing a deadlock predicate such that satisfiability is a necessary and sufficient condition for total deadlock. We describe a technique for synthesizing a generalized deadlock predicate such that satisfiability is a necessary and sufficient condition for both total and partial deadlock. Our method constructs a strongest resource invariant using Clarke's fixed point functional. We then use this strongest resource invariant and a predicate transformer to construct a generalized deadlock predicate.