Checking and enforcing robustness against TSO

DOI10.1007/978-3-642-37036-6_29MaRDI QIDQ5326306zbMATH OpenOpenAlexFDO

Authors Ahmed Bouajjani, Egor Derevenetc, Roland Meyer

Publication date 5 August 2013

Published in Programming Languages and Systems (Search for Journal in Brave)

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

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) Analysis of algorithms and problem complexity (68Q25) Semantics in the theory of computing (68Q55)

Abstract: We present algorithms for checking and enforcing robustness of concurrent programs against the Total Store Ordering (TSO) memory model. A program is robust if all its TSO computations correspond to computations under the Sequential Consistency (SC) semantics. We provide a complete characterization of non-robustness in terms of so-called attacks: a restricted form of (harmful) out-of-program-order executions. Then, we show that detecting attacks can be parallelized, and can be solved using state reachability queries under SC semantics in a suitably instrumented program obtained by a linear size source-to-source translation. Importantly, the construction is valid for an arbitrary number of addresses and an arbitrary number of parallel threads, and it is independent from the data domain and from the size of store buffers in the TSO semantics. In particular, when the data domain is finite and the number of addresses is fixed, we obtain decidability and complexity results for robustness, even for an arbitrary number of threads. As a second contribution, we provide an algorithm for computing an optimal set of fences that enforce robustness. We consider two criteria of optimality: minimization of program size and maximization of its performance. The algorithms we define are implemented, and we successfully applied them to analyzing and correcting several concurrent algorithms.

Recommendations

• Deciding Robustness against Total Store Ordering
• Reasoning about TSO programs using reduction and abstraction
• Counter-Example Guided Fence Insertion under TSO
• On atomicity in presence of non-atomic writes
• Robustness against Power is PSpace-complete

Cited in

(20)

• Stateless model checking for TSO and PSO
• Parameterized model checking on the TSO weak memory model
• Checking robustness between weak transactional consistency models
• On atomicity in presence of non-atomic writes
• CCA-secure keyed-fully homomorphic encryption
• A theory of partitioned global address spaces
• Verifying robustness of event-driven asynchronous programs against concurrency
• Mending fences with self-invalidation and self-downgrade
• A load-buffer semantics for total store ordering
• Algebraic laws for weak consistency
• Robustness against Power is PSpace-complete
• Context-bounded analysis of TSO systems
• From total store order to sequential consistency: a practical reduction theorem
• scientific article; zbMATH DE number 7327945 (Why is no real title available?)
• Robustness Against Transactional Causal Consistency.
• Decidability of liveness for concurrent objects on the TSO memory model
• Parameterized verification under TSO with data types
• TSO games -- on the decidability of safety games under the total store order semantics
• TSO games -- on the decidability of safety games under the total store order semantics
• Linearizability on hardware weak memory models

This page was built for publication: Checking and enforcing robustness against TSO

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