Discovering and correcting a deadlock in a channel implementation

DOI10.1007/S00165-019-00487-YMaRDI QIDQ2322306zbMATH OpenOpenAlexWikidataFDO

Authors Gavin Lowe

Publication date 4 September 2019

Published in Formal Aspects of Computing (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/s00165-019-00487-y

zbMATH Keywords

channel implementationCSPmessage-passing concurrencymodel checking

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Deadlock-free channels and locks
• scientific article; zbMATH DE number 1231692
• A CCS-based investigation of deadlock in a multi-process electronic mail system
• Deadlock analysis in networks of communicating processes
• \(\text{DELFIN}^+\): an efficient deadlock detection tool for CCS processes

Cites work

• Communicating Sequential Processes. The First 25 Years
• Deadlock analysis in networks of communicating processes
• FDR3 -- a modern refinement checker for CSP
• Model-checking CSP-Z: Strategy, tool support and industrial application
• The automatic detection of token structures and invariants using SAT checking
• The pursuit of deadlock freedom
• Tighter reachability criteria for deadlock-freedom analysis
• Understanding concurrent systems
• View abstraction for systems with component identities

Cited in

(3)

• Deadlock-free channels and locks
• Searching for deadlocks while debugging Concurrent Haskell programs
• Toward verifying cooperatively scheduled runtimes using CSP

Describes a project that uses

Uses Software

• FDR3

This page was built for publication: Discovering and correcting a deadlock in a channel implementation

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