Item Details

Synthesizing a General Deadlock Predicate

OHallaron, David; Reynolds, Paul
Format
Report
Author
OHallaron, David
Reynolds, Paul
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.
Language
English
Published
University of Virginia, Department of Computer Science, 1985
Published Date
1985
Collection
Libra Open Repository
Logo for In CopyrightIn Copyright

Availability

Access Online