Context-bounded analysis of TSO systems

DOI10.1007/978-3-642-54848-2_2MaRDI QIDQ5170741zbMATH OpenOpenAlexFDO

Authors Mohamed Faouzi Atig, Ahmed Bouajjani, Gennaro Parlato

Publication date 24 July 2014

Published in From Programs to Systems. The Systems perspective in Computing (Search for Journal in Brave)

Full work available at URL https://eprints.soton.ac.uk/365362/1/WMM.pdf

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) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• On the verification problem for weak memory models
• Bounded TSO-to-SC linearizability is decidable
• Counter-Example Guided Fence Insertion under TSO
• What's decidable about weak memory models?
• Context-Bounded Analysis of Concurrent Queue Systems

Cites work

• Checking and enforcing robustness against TSO
• Context-Bounded Analysis for Concurrent Programs with Dynamic Creation of Threads
• Counter-Example Guided Fence Insertion under TSO
• Deciding Robustness against Total Store Ordering
• Effective Program Verification for Relaxed Memory Models
• Emptiness of Multi-pushdown Automata Is 2ETIME-Complete
• Formalising Java’s Data Race Free Guarantee
• scientific article; zbMATH DE number 1517989 (Why is no real title available?)
• Interprocedural Analysis of Concurrent Programs Under a Context Bound
• On the verification problem for weak memory models
• Reducing Concurrent Analysis Under a Context Bound to Sequential Analysis
• Reducing Context-Bounded Concurrent Reachability to Sequential Reachability
• Relaxed memory models
• Scope-bounded pushdown languages
• Software verification for weak memory via program transformation
• Sound and complete monitoring of sequential consistency for relaxed memory models
• The tree width of auxiliary storage
• Tools and Algorithms for the Construction and Analysis of Systems
• What's decidable about weak memory models?

Cited in

(8)

• The decidability of verification under PS 2.0
• scientific article; zbMATH DE number 1670756 (Why is no real title available?)
• Bounded TSO-to-SC linearizability is decidable
• What's decidable about weak memory models?
• Unifying Operational Weak Memory Verification: An Axiomatic Approach
• scientific article; zbMATH DE number 7327945 (Why is no real title available?)
• Probabilistic total store ordering
• Reconciling preemption bounding with DPOR

Describes a project that uses

Uses Software

• Memorax

This page was built for publication: Context-bounded analysis of TSO systems

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