Reasoning about TSO programs using reduction and abstraction

Ahmed Bouajjani; Constantin Enea; Suha Orhun Mutluergil; Serdar Tasiran

doi:10.1007/978-3-319-96142-2_21

Reasoning about TSO programs using reduction and abstraction

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

Université Paris 7
Koç University School of Medicine
Amazon Machine Learning Solutions Lab

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

14 Citations (Scopus)

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.

Original language	English
Title of host publication	Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings
Editors	Georg Weissenbacher, Hana Chockler
Publisher	Springer Verlag
Pages	336-353
Number of pages	18
ISBN (Print)	9783319961415
DOIs	https://doi.org/10.1007/978-3-319-96142-2_21
Publication status	Published - 1 Jan 2018
Externally published	Yes
Event	30th International Conference on Computer Aided Verification, CAV 2018 Held as Part of the Federated Logic Conference, FloC 2018 - Oxford, United Kingdom Duration: 14 Jul 2018 → 17 Jul 2018

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	10982 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	30th International Conference on Computer Aided Verification, CAV 2018 Held as Part of the Federated Logic Conference, FloC 2018
Country/Territory	United Kingdom
City	Oxford
Period	14/07/18 → 17/07/18

Access to Document

10.1007/978-3-319-96142-2_21

Cite this

Bouajjani, A., Enea, C., Mutluergil, S. O., & Tasiran, S. (2018). Reasoning about TSO programs using reduction and abstraction. In G. Weissenbacher, & H. Chockler (Eds.), Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings (pp. 336-353). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10982 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-319-96142-2_21

Bouajjani, Ahmed ; Enea, Constantin ; Mutluergil, Suha Orhun et al. / Reasoning about TSO programs using reduction and abstraction. Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings. editor / Georg Weissenbacher ; Hana Chockler. Springer Verlag, 2018. pp. 336-353 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{7a8f8637000946c5b09ab612d352ffe7,

title = "Reasoning about TSO programs using reduction and abstraction",

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{\textquoteright}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.",

author = "Ahmed Bouajjani and Constantin Enea and Mutluergil, \{Suha Orhun\} and Serdar Tasiran",

note = "Publisher Copyright: {\textcopyright} The Author(s) 2018.; 30th International Conference on Computer Aided Verification, CAV 2018 Held as Part of the Federated Logic Conference, FloC 2018 ; Conference date: 14-07-2018 Through 17-07-2018",

year = "2018",

month = jan,

day = "1",

doi = "10.1007/978-3-319-96142-2\_21",

language = "English",

isbn = "9783319961415",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "336--353",

editor = "Georg Weissenbacher and Hana Chockler",

booktitle = "Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings",

}

Bouajjani, A, Enea, C, Mutluergil, SO & Tasiran, S 2018, Reasoning about TSO programs using reduction and abstraction. in G Weissenbacher & H Chockler (eds), Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 10982 LNCS, Springer Verlag, pp. 336-353, 30th International Conference on Computer Aided Verification, CAV 2018 Held as Part of the Federated Logic Conference, FloC 2018, Oxford, United Kingdom, 14/07/18. https://doi.org/10.1007/978-3-319-96142-2_21

Reasoning about TSO programs using reduction and abstraction. / Bouajjani, Ahmed; Enea, Constantin; Mutluergil, Suha Orhun et al.
Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings. ed. / Georg Weissenbacher; Hana Chockler. Springer Verlag, 2018. p. 336-353 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10982 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Reasoning about TSO programs using reduction and abstraction

AU - Bouajjani, Ahmed

AU - Enea, Constantin

AU - Mutluergil, Suha Orhun

AU - Tasiran, Serdar

PY - 2018/1/1

Y1 - 2018/1/1

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-319-96142-2_21

DO - 10.1007/978-3-319-96142-2_21

M3 - Conference contribution

AN - SCOPUS:85051145992

SN - 9783319961415

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 336

EP - 353

BT - Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings

A2 - Weissenbacher, Georg

A2 - Chockler, Hana

PB - Springer Verlag

T2 - 30th International Conference on Computer Aided Verification, CAV 2018 Held as Part of the Federated Logic Conference, FloC 2018

Y2 - 14 July 2018 through 17 July 2018

ER -

Bouajjani A, Enea C, Mutluergil SO, Tasiran S. Reasoning about TSO programs using reduction and abstraction. In Weissenbacher G, Chockler H, editors, Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings. Springer Verlag. 2018. p. 336-353. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-319-96142-2_21

Reasoning about TSO programs using reduction and abstraction

Abstract

Publication series

Conference

Access to Document

Fingerprint

Cite this