We introduce some combinatorial techniques for establishing the deadlock freedom of concurrent systems which are similar to the variant/invariant method of proving loop termination. Our methods are based on the local analysis of networks, which is combinatorially far easier than analysing all global states. They are illustrated by proving numerous examples to be free of deadlock, some of which are useful classes of network.
Recommendations
Cites work
- A Proof System for Communicating Sequential Processes
- A Theory of Communicating Sequential Processes
- Deadlock absence proofs for networks of communicating processes
- scientific article; zbMATH DE number 3902016 (Why is no real title available?)
- scientific article; zbMATH DE number 3926230 (Why is no real title available?)
- scientific article; zbMATH DE number 4039251 (Why is no real title available?)
- scientific article; zbMATH DE number 3711387 (Why is no real title available?)
- Verifying properties of parallel programs
Cited in
(29)- A generalized deadlock predicate
- A deadlock free and starvation free network of packet switching communication processors
- Reducing complex CSP models to traces via priority
- Using partial orders for the efficient verification of deadlock freedom and safety properties
- Checking deadlock-freedom of parametric component-based systems
- Translating between models of concurrency
- Tighter reachability criteria for deadlock-freedom analysis
- Discovering and correcting a deadlock in a channel implementation
- Efficient verification of concurrent systems using local-analysis-based approximations and SAT solving
- A trace-based service semantics guaranteeing deadlock freedom
- Deadlock analysis in networks of communicating processes
- Verifying deadlock-freedom of communication fabrics
- Deadlock analysis of unbounded process networks
- scientific article; zbMATH DE number 3862446 (Why is no real title available?)
- Deadlock free specification based on local process properties
- scientific article; zbMATH DE number 3926230 (Why is no real title available?)
- scientific article; zbMATH DE number 176516 (Why is no real title available?)
- scientific article; zbMATH DE number 1088044 (Why is no real title available?)
- Proof pearl: a formal proof of Dally and Seitz' necessary and sufficient condition for deadlock-free routing in interconnection networks
- Deadlock checking by a behavioral effect system for lock handling
- Static deadlock prevention in dynamically configured communication networks
- Component-Based Construction of Deadlock-Free Systems
- A formal proof of a necessary and sufficient condition for deadlock-free adaptive networks
- A Livelock Freedom Analysis for Infinite State Asynchronous Reactive Systems
- Wait-freedom with advice
- Wait-freedom with advice
- Checking deadlock-freedom of parametric component-based systems
- Deadlock-freeness of hexagonal systolic arrays
- Deadlock-freedom in resource contentions
This page was built for publication: The pursuit of deadlock freedom
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q580970)
