Context-Bounded Analysis for Concurrent Programs with Dynamic Creation of Threads

DOI10.1007/978-3-642-00768-2_11MaRDI QIDQ3617755zbMATH OpenOpenAlexFDO

Authors Mohamed Faouzi Atig, Ahmed Bouajjani, Shaz Qadeer

Publication date 31 March 2009

Published in Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

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

Mathematics Subject Classification ID

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

Abstract: Context-bounded analysis has been shown to be both efficient and effective at finding bugs in concurrent programs. According to its original definition, context-bounded analysis explores all behaviors of a concurrent program up to some fixed number of context switches between threads. This definition is inadequate for programs that create threads dynamically because bounding the number of context switches in a computation also bounds the number of threads involved in the computation. In this paper, we propose a more general definition of context-bounded analysis useful for programs with dynamic thread creation. The idea is to bound the number of context switches for each thread instead of bounding the number of switches of all threads. We consider several variants based on this new definition, and we establish decidability and complexity results for the analysis induced by them.

Recommendations

• Context-bounded analysis for concurrent programs with dynamic creation of threads
• Context-Bounded Analysis of Multithreaded Programs with Dynamic Linked Structures
• Reducing Concurrent Analysis Under a Context Bound to Sequential Analysis
• Reducing concurrent analysis under a context bound to sequential analysis
• Interprocedural Analysis of Concurrent Programs Under a Context Bound

Cites work

• Automata, Languages and Programming
• Automated Deduction – CADE-20
• Context-bounded analysis for concurrent programs with dynamic creation of threads
• Expand, enlarge and check: new algorithms for the coverability problem of WSTS
• FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science
• scientific article; zbMATH DE number 10087 (Why is no real title available?)
• scientific article; zbMATH DE number 762060 (Why is no real title available?)
• Interprocedural Analysis of Concurrent Programs Under a Context Bound
• Reducing Concurrent Analysis Under a Context Bound to Sequential Analysis
• The covering and boundedness problems for vector addition systems
• Tools and Algorithms for the Construction and Analysis of Systems
• Verification, Model Checking, and Abstract Interpretation

Cited in

(18)

• Reducing concurrent analysis under a context bound to sequential analysis
• General decidability results for asynchronous shared-memory programs: higher-order and beyond
• Reachability of scope-bounded multistack pushdown systems
• Join-Lock-Sensitive Forward Reachability Analysis for Concurrent Programs with Dynamic Process Creation
• Reachability of multistack pushdown systems with scope-bounded matching relations
• Reasoning about threads with bounded lock chains
• Contextual effects for version-consistent dynamic software updating and safe concurrent programming
• Context-bounded analysis for concurrent programs with dynamic creation of threads
• Reducing Concurrent Analysis Under a Context Bound to Sequential Analysis
• Precise Fixpoint-Based Analysis of Programs with Thread-Creation and Procedures
• Bounded context switching for valence systems
• General Decidability Results for Asynchronous Shared-Memory Programs: Higher-Order and Beyond
• Context-bounded analysis of TSO systems
• Context-Bounded Analysis of Multithreaded Programs with Dynamic Linked Structures
• Interprocedural Analysis of Concurrent Programs Under a Context Bound
• Tools and Algorithms for the Construction and Analysis of Systems
• Fine-grained complexity of safety verification
• The complexity of bounded context switching with dynamic thread creation

This page was built for publication: Context-Bounded Analysis for Concurrent Programs with Dynamic Creation of Threads

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