Synthesizing a General Deadlock Predicate

Report
Authors:OHallaron, David, Department of Computer ScienceUniversity of Virginia Reynolds, Paul, Department of Computer ScienceUniversity of Virginia
Abstract:

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.

Rights:
All rights reserved (no additional license for public reuse)
Language:
English
Source Citation:

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

Publisher:
University of Virginia, Department of Computer Science
Published Date:
1985