Deadlock detection in linear recursive programs

DOI10.1007/978-3-319-07317-0_2MaRDI QIDQ5175772zbMATH OpenOpenAlexFDO

Authors Elena Giachino, Cosimo Laneve

Publication date 25 February 2015

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1310.7449

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Abstract: Deadlock detection in recursive programs that admit dynamic resource creation is extremely complex and solutions either give imprecise answers or do not scale. We define an algorithm for detecting deadlocks of "linear recursive programs" of a basic model. The theory that underpins the algorithm is a generalization of the theory of permutations of names to so-called "mutations", which transform tuples by introducing duplicates and fresh names. Our algorithm realizes the back-end of deadlock analyzers for object-oriented programming languages, once the association programs/basic-model-programs has been defined as front-end.

Recommendations

• Deadlock analysis of unbounded process networks
• Deadlock analysis of unbounded process networks
• Loops, ditopology and deadlocks
• Deadlock checking by data race detection
• Resource-Oriented Deadlock Analysis

Cites work

• A calculus of communicating systems
• A calculus of mobile processes. II
• A generic type system for the pi-calculus
• A New Type System for Deadlock-Free Processes
• A Theory of Communicating Sequential Processes
• Analysis of recursively parallel programs
• Asynchronous and deterministic objects
• Automata and Logics for Words and Trees over an Infinite Alphabet
• Depth-First Search and Linear Graph Algorithms
• scientific article; zbMATH DE number 1231616 (Why is no real title available?)
• scientific article; zbMATH DE number 3443655 (Why is no real title available?)
• scientific article; zbMATH DE number 1834677 (Why is no real title available?)
• The Must Preorder Revisited
• Types and typechecking for Communicating Quantum Processes
• Types as models: model checking message-passing programs

Cited in

(9)

• Deadlock detection of Java bytecode
• A lightweight deadlock analysis for programs with threads and reentrant locks
• Deadlock analysis of unbounded process networks
• Effect-polymorphic behaviour inference for deadlock checking
• Automated deadlock detection in synchronized reentrant multithreaded call-graphs
• Termination, deadlock, and divergence
• Loops, ditopology and deadlocks
• Deadlock detection in MPI programs
• Deadlock analysis of unbounded process networks

Describes a project that uses

Uses Software

• TyPiCal
• PIPER
• ABS

This page was built for publication: Deadlock detection in linear recursive programs

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