Model Checking of C++ Programs Under the x86-TSO Memory Model

D 2018

Model Checking of C++ Programs Under the x86-TSO Memory Model

ŠTILL, Vladimír a Jiří BARNAT

Základní údaje

Originální název

Model Checking of C++ Programs Under the x86-TSO Memory Model

Autoři

ŠTILL, Vladimír (203 Česká republika, garant, domácí) a Jiří BARNAT (203 Česká republika, domácí)

Vydání

Cham, Formal Methods and Software Engineering, od s. 124-140, 17 s. 2018

Nakladatel

Springer

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10200 1.2 Computer and information sciences

Stát vydavatele

Švýcarsko

Utajení

není předmětem státního či obchodního tajemství

Forma vydání

tištěná verze "print"

Odkazy

Publisher's page Author's page

Impakt faktor

Impact factor: 0.402 v roce 2005

Kód RIV

RIV/00216224:14330/18:00101450

Organizační jednotka

Fakulta informatiky

ISBN

978-3-030-02449-9

ISSN

DOI

http://dx.doi.org/10.1007/978-3-030-02450-5_8

UT WoS

000672801600008

Klíčová slova anglicky

relaxed memory; model checking; c++; x86; memory model; DIVINE

Štítky

core_B, firank_B

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 30. 4. 2019 07:36, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

In this work, we present an extension of the DIVINE model checker that allows for analysis of C and C++ programs under the Open image in new window relaxed memory model. We use an approach in which the program to be verified is first transformed, so that it itself encodes the relaxed memory behavior, and after that it is verified by an explicit-state model checker supporting only the standard sequentially consistent memory. The novelty of our approach is in a careful design of an encoding of Open image in new window operations so that the nondeterminism introduced by the relaxed memory simulation is minimized. In particular, we allow for nondeterminism only in connection with memory fences and load operations of those memory addresses that were written to by a preceding store. We evaluate and compare our approach with the state-of-the-art bounded model checker CBMC and stateless model checker Nidhugg. For the comparison we employ SV-COMP concurrency benchmarks that do not exhibit data nondeterminism, and we show that our solution built on top of the explicit-state model checker outperforms both of the other tools. The implementation is publicly available as an open source software.

Návaznosti

GA18-02177S, projekt VaV

Název: Abstrakce a jiné techniky v semi-symbolické verifikaci programů

Investor: Grantová agentura ČR, Abstrakce a jiné techniky v semi-symbolické verifikaci programů

MUNI/A/0854/2017, interní kód MU

Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VII.

Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VII., DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty

MUNI/A/1038/2017, interní kód MU

Název: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity 18

Investor: Masarykova univerzita, Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity 18, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty

Citovat

ŠTILL, Vladimír a Jiří BARNAT. Model Checking of C++ Programs Under the x86-TSO Memory Model. In Jing Sun, Meng Sun. Formal Methods and Software Engineering. Cham: Springer, 2018, s. 124-140. ISBN 978-3-030-02449-9. Dostupné z: https://dx.doi.org/10.1007/978-3-030-02450-5_8.

@inproceedings{1479960,
   author = {Štill, Vladimír and Barnat, Jiří},
   address = {Cham},
   booktitle = {Formal Methods and Software Engineering},
   doi = {http://dx.doi.org/10.1007/978-3-030-02450-5_8},
   editor = {Jing Sun, Meng Sun},
   keywords = {relaxed memory; model checking; c++; x86; memory model; DIVINE},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {Cham},
   isbn = {978-3-030-02449-9},
   pages = {124-140},
   publisher = {Springer},
   title = {Model Checking of C++ Programs Under the x86-TSO Memory Model},
   url = {https://link.springer.com/chapter/10.1007%2F978-3-030-02450-5_8},
   year = {2018}
}

TY  - JOUR
ID  - 1479960
AU  - Štill, Vladimír - Barnat, Jiří
PY  - 2018
TI  - Model Checking of C++ Programs Under the x86-TSO Memory Model
PB  - Springer
CY  - Cham
SN  - 9783030024499
KW  - relaxed memory
KW  - model checking
KW  - c++
KW  - x86
KW  - memory model
KW  - DIVINE
UR  - https://link.springer.com/chapter/10.1007%2F978-3-030-02450-5_8
L2  - https://link.springer.com/chapter/10.1007%2F978-3-030-02450-5_8
N2  - In this work, we present an extension of the DIVINE model checker that allows for analysis of C and C++ programs under the Open image in new window relaxed memory model. We use an approach in which the program to be verified is first transformed, so that it itself encodes the relaxed memory behavior, and after that it is verified by an explicit-state model checker supporting only the standard sequentially consistent memory. The novelty of our approach is in a careful design of an encoding of Open image in new window operations so that the nondeterminism introduced by the relaxed memory simulation is minimized. In particular, we allow for nondeterminism only in connection with memory fences and load operations of those memory addresses that were written to by a preceding store. We evaluate and compare our approach with the state-of-the-art bounded model checker CBMC and stateless model checker Nidhugg. For the comparison we employ SV-COMP concurrency benchmarks that do not exhibit data nondeterminism, and we show that our solution built on top of the explicit-state model checker outperforms both of the other tools. The implementation is publicly available as an open source software.
ER  -

ŠTILL, Vladimír a Jiří BARNAT. Model Checking of C++ Programs Under the x86-TSO Memory Model. In Jing Sun, Meng Sun. \textit{Formal Methods and Software Engineering}. Cham: Springer, 2018, s.~124-140. ISBN~978-3-030-02449-9. Dostupné z: https://dx.doi.org/10.1007/978-3-030-02450-5\_{}8.

Podrobný výpis o publikaci