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
Date Received
20121029
Published
University of Virginia, Department of Computer Science, 1985
Published Date
1985
Collection
Libra Open Repository
Logo for In CopyrightIn Copyright

Availability

Access Online