Item Details

Print View

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
2012-10-29
Published
University of Virginia, Department of Computer Science, 1985
Published Date
1985
Collection
Libra Open Repository
In CopyrightIn Copyright
▾See more
▴See less

Availability

Access Online