Deadlock checking by a behavioral effect system for lock handling

DOI10.1016/J.JLAP.2011.11.001MaRDI QIDQ444480zbMATHOpenAlexFDO

Authors Ka I Pun, Martin Steffen, Volker Stolz

Publication date 14 August 2012

Published in The Journal of Logic and Algebraic Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.jlap.2011.11.001

zbMATH Keywords

abstractionconcurrencystatic analysisdeadlock preventionbehavioral type and effect systemssimulation relation

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Deadlock checking by data race detection
• Deadlock checking by data race detection
• Effect-polymorphic behaviour inference for deadlock checking
• A lightweight deadlock analysis for programs with threads and reentrant locks
• Deadlock-free channels and locks

Cites work

• scientific article; zbMATH DE number 1670775 (Why is no real title available?)
• scientific article; zbMATH DE number 3967878 (Why is no real title available?)
• scientific article; zbMATH DE number 4037177 (Why is no real title available?)
• scientific article; zbMATH DE number 1324833 (Why is no real title available?)
• scientific article; zbMATH DE number 1759631 (Why is no real title available?)
• scientific article; zbMATH DE number 7088727 (Why is no real title available?)
• scientific article; zbMATH DE number 3359777 (Why is no real title available?)
• A New Type System for Deadlock-Free Processes
• A generic type system for the \(\pi\)-calculus
• Automated deadlock detection in synchronized reentrant multithreaded call-graphs
• Computer Aided Verification
• Conditional must not aliasing for static race detection
• Deadlock checking by a behavioral effect system for lock handling
• Inferring Channel Buffer Bounds Via Linear Programming
• Refinement of actions and equivalence notions for concurrent systems
• Searching for deadlocks while debugging Concurrent Haskell programs
• Static deadlock prevention in dynamically configured communication networks
• Temporal Assertions with Parametrized Propositions
• The pursuit of deadlock freedom
• Type-based information flow analysis for the \(\pi\)-calculus
• Types and Deadlock Freedom in a Calculus of Services, Sessions and Pipelines
• ν-Types for Effects and Freshness Analysis

Cited in

(7)

• Deadlock checking by data race detection
• Deadlock checking by data race detection
• Deadlock-free channels and locks
• Deadlock Analysis of Wait-Notify Coordination
• A lightweight deadlock analysis for programs with threads and reentrant locks
• Deadlock checking by a behavioral effect system for lock handling
• Effect-polymorphic behaviour inference for deadlock checking

Describes a project that uses

Uses Software

• Haskell
• Cyclone
• RacerX

This page was built for publication: Deadlock checking by a behavioral effect system for lock handling

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