FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
Reasoning About TSO Programs Using Reduction and Abstraction

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

Paper Information

Title:Reasoning About TSO Programs Using Reduction and Abstraction
Authors:Ahmed Bouajjani, Constantin Enea, Suha Orhun Mutluergil and Serdar Tasiran
Proceedings:CAV All Papers
Editors: Georg Weissenbacher, Hana Chockler and Igor Konnov
Keywords:Total Store Ordering, Robustness, Reduction, Abstraction
Abstract:

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.

Pages:18
Talk:Jul 17 14:15 (Session 121A: Concurrency)
Paper: