Weak Memory Models as LLVM-to-LLVM Transformations

D 2016

Weak Memory Models as LLVM-to-LLVM Transformations

ŠTILL, Vladimír, Petr ROČKAI a Jiří BARNAT

Základní údaje

Originální název

Weak Memory Models as LLVM-to-LLVM Transformations

Autoři

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

Vydání

Neuveden, Mathematical and Engineering Methods in Computer Science - 10th International Doctoral Workshop, od s. 144-155, 12 s. 2016

Nakladatel

Springer

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Švýcarsko

Utajení

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

Forma vydání

elektronická verze "online"

Odkazy

URL

Impakt faktor

Impact factor: 0.402 v roce 2005

Kód RIV

RIV/00216224:14330/16:00088094

Organizační jednotka

Fakulta informatiky

ISBN

978-3-319-29816-0

ISSN

DOI

http://dx.doi.org/10.1007/978-3-319-29817-7_13

UT WoS

000374173700013

Klíčová slova anglicky

memory models; model checking

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 13. 5. 2020 19:15, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

Data races are among the most difficult software bugs to discover. They arise from multiple threads accessing the same memory location, a situation which is often hard to discern from source code alone. Detection of such bugs is further complicated by individual CPUs’ use of relaxed memory models. As a matter of fact, proving absence of data races is a typical task for automated formal verification. In this paper, we present a new approach for verification of multi-threaded C and C++ programs under weakened memory models (using store buffer emulation), using an unmodified model checker that assumes Sequential Consistency. In our workflow, a C or C++ program is translated into LLVM bitcode, which is then automatically extended with store buffer emulation. After this transformation, the extended LLVM bitcode is model-checked against safety and/or liveness properties with our explicit-state model checker DIVINE.

Návaznosti

GA15-08772S, projekt VaV

Název: Analýza korektnosti vícevláknových programů v C a C++

Investor: Grantová agentura ČR, Correctness Analysis of C and C++ Programs with Threads

Citovat

ŠTILL, Vladimír, Petr ROČKAI a Jiří BARNAT. Weak Memory Models as LLVM-to-LLVM Transformations. Online. In Jan Kofroň and Tomáš Vojnar. Mathematical and Engineering Methods in Computer Science - 10th International Doctoral Workshop. Neuveden: Springer, 2016, s. 144-155. ISBN 978-3-319-29816-0. Dostupné z: https://dx.doi.org/10.1007/978-3-319-29817-7_13.

@inproceedings{1352236,
   author = {Štill, Vladimír and Ročkai, Petr and Barnat, Jiří},
   address = {Neuveden},
   booktitle = {Mathematical and Engineering Methods in Computer Science - 10th International Doctoral Workshop},
   doi = {http://dx.doi.org/10.1007/978-3-319-29817-7_13},
   editor = {Jan Kofroň and Tomáš Vojnar},
   keywords = {memory models; model checking},
   howpublished = {elektronická verze "online"},
   language = {eng},
   location = {Neuveden},
   isbn = {978-3-319-29816-0},
   pages = {144-155},
   publisher = {Springer},
   title = {Weak Memory Models as LLVM-to-LLVM Transformations},
   url = {http://dx.doi.org/10.1007/978-3-319-29817-7_13},
   year = {2016}
}

TY  - JOUR
ID  - 1352236
AU  - Štill, Vladimír - Ročkai, Petr - Barnat, Jiří
PY  - 2016
TI  - Weak Memory Models as LLVM-to-LLVM Transformations
PB  - Springer
CY  - Neuveden
SN  - 9783319298160
KW  - memory models
KW  - model checking
UR  - http://dx.doi.org/10.1007/978-3-319-29817-7_13
N2  - Data races are among the most difficult software bugs to discover. They arise from multiple threads accessing the same memory location, a situation which is often hard to discern from source code alone. Detection of such bugs is further complicated by individual CPUs’ use of relaxed memory models. As a matter of fact, proving absence of data races is a typical task for automated formal verification. In this paper, we present a new approach for verification of multi-threaded C and C++ programs under weakened memory models (using store buffer emulation), using an unmodified model checker that assumes Sequential Consistency. In our workflow, a C or C++ program is translated into LLVM bitcode, which is then automatically extended with store buffer emulation. After this transformation, the extended LLVM bitcode is model-checked against safety and/or liveness properties with our explicit-state model checker DIVINE.
ER  -

ŠTILL, Vladimír, Petr ROČKAI a Jiří BARNAT. Weak Memory Models as LLVM-to-LLVM Transformations. Online. In Jan Kofroň and Tomáš Vojnar. \textit{Mathematical and Engineering Methods in Computer Science - 10th International Doctoral Workshop}. Neuveden: Springer, 2016, s.~144-155. ISBN~978-3-319-29816-0. Dostupné z: https://dx.doi.org/10.1007/978-3-319-29817-7\_{}13.

Podrobný výpis o publikaci