A generalized deadlock predicate

DOI10.1016/0020-0190(86)90133-XMaRDI QIDQ1085972zbMATH OpenOpenAlexFDO

Authors David R. O'Hallaron, Paul Reynolds

Publication date 1986

Published in Information Processing Letters (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0020-0190(86)90133-x

zbMATH Keywords

fixed point functionaloperating systemparallel processingpredicate transformerresource invariantsemaphore invariant methodsoftware reliability

Mathematics Subject Classification ID

Theory of operating systems (68N25)

Review text

Satisfiability of the deadlock predicate contructed by the semaphore invariant method is a necessary condition for total deadlock in PV programs. \textit{E. M. Clarke jun.} [ACM Trans. Program. Lang. Syst. 2, 338-358 (1980; Zbl 0468.68024)] has developed a technique, based on a view of resource invariants as fixed points 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 generalized 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 a predicate transformer to construct a generalized deadlock predicate.

Recommendations

• Verification, Model Checking, and Abstract Interpretation
• The pursuit of deadlock freedom
• Two logical methods of deadlock analysis
• Cut-off theorems for the \textit{PV}-model
• Resource-Oriented Deadlock Analysis

Cites work

• Formal derivation of strongly correct concurrent programs
• scientific article; zbMATH DE number 3463159 (Why is no real title available?)
• Programming as a Discipline of Mathematical Nature
• Synchronization Problems Solvable by Generalized PV Systems
• Synthesis of Resource Invariants for Concurrent Programs
• The Total Correctness of Parallel Programs
• Verifying properties of parallel programs

Cited in

(1)

• Cut-off theorems for the \textit{PV}-model

This page was built for publication: A generalized deadlock predicate

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1085972)