Synthesizing a General Deadlock PredicateReport
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.
All rights reserved (no additional license for public reuse)
OHallaron, David, and Paul Reynolds. "Synthesizing a General Deadlock Predicate." University of Virginia Dept. of Computer Science Tech Report (1985).
University of Virginia, Department of Computer Science