Reasoning about TSO programs using reduction and abstraction

DOI10.1007/978-3-319-96142-2_21MaRDI QIDQ6039412zbMATH OpenFDO

Authors Ahmed Bouajjani, Constantin Enea, Suha Orhun Mutluergil, Serdar Tasiran

Publication date 5 May 2023

Published in Computer Aided Verification (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

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

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Semantics in the theory of computing (68Q55) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Abstract: We present a method for proving that a program running under the Total Store Ordering (TSO) memory model is robust, i.e., all its TSO computations are equivalent to computations under the Sequential Consistency (SC) semantics. This method is inspired by Lipton's reduction theory for proving atomicity of concurrent programs. For programs which are not robust, we introduce an abstraction mechanism that allows to construct robust programs over-approximating their TSO semantics. This enables the use of proof methods designed for the SC semantics in proving invariants that hold on the TSO semantics of a non-robust program. These techniques have been evaluated on a large set of benchmarks using the infrastructure provided by CIVL, a generic tool for reasoning about concurrent programs under the SC semantics.

Recommendations

• Reasoning algebraically about refinement on TSO architectures
• scientific article; zbMATH DE number 890353
• A Proof-Theoretic Account of Programming and the Role of Reduction Rules
• scientific article; zbMATH DE number 2110619
• Simplifying linearizability proofs with reduction and abstraction
• A CTL-based logic for program abstractions
• Predicate abstraction for program verification
• Program synthesis with equivalence reduction

Cited in

(6)

• Checking and enforcing robustness against TSO
• From total store order to sequential consistency: a practical reduction theorem
• A high-level semantics for program execution under total store order memory
• Robustness against Power is PSpace-complete
• Reasoning algebraically about refinement on TSO architectures
• Show no weakness: sequentially consistent specifications of TSO libraries

This page was built for publication: Reasoning about TSO programs using reduction and abstraction

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