Synthesizing a General Deadlock Predicate

Satisfiability of the deadlock predicate constructed by the semaphore invariant method is a necessary condition for total deadlock in PV programs. Clarke has developed a technique, based on a view of resource invariants as fixpoints 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 general 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 an inverse fixed point functional to construct a general deadlock predicate.

OHallaron, David, and Paul Reynolds. "Synthesizing a General Deadlock Predicate." University of Virginia Dept. of Computer Science Tech Report (1985).