Deadlock checking by a behavioral effect system for lock handling

DOI10.1016/J.JLAP.2011.11.001zbMATH Open1246.68097OpenAlexW2084800560MaRDI QIDQ444480FDOQ444480

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

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

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)

Cites Work

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

Cited In (4)

• Deadlock-free channels and locks
• Deadlock checking by data race detection
• Effect-polymorphic behaviour inference for deadlock checking
• Deadlock checking by a behavioral effect system for lock handling

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)