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

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F18%3A00101450" target="_blank" >RIV/00216224:14330/18:00101450 - isvavai.cz</a>

Výsledek na webu

<a href="https://link.springer.com/chapter/10.1007%2F978-3-030-02450-5_8" target="_blank" >https://link.springer.com/chapter/10.1007%2F978-3-030-02450-5_8</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-030-02450-5_8" target="_blank" >10.1007/978-3-030-02450-5_8</a>

Jazyk výsledku

angličtina

Název v původním jazyce

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

Popis výsledku v původním jazyce

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ázev v anglickém jazyce

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

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

10200 - Computer and information sciences

Projekt

<a href="/cs/project/GA18-02177S" target="_blank" >GA18-02177S: Abstrakce a jiné techniky v semi-symbolické verifikaci programů</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění

2018

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

Formal Methods and Software Engineering

ISBN

9783030024499

ISSN

0302-9743

e-ISSN

—

Počet stran výsledku

17

Strana od-do

124-140

Název nakladatele

Springer

Místo vydání

Cham

Místo konání akce

Gold Coast, Austrálie

Datum konání akce

1. 1. 2018

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

—