Weak Memory Models as LLVM-to-LLVM Transformations

D 2016

Weak Memory Models as LLVM-to-LLVM Transformations

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

Basic information

Original name

Weak Memory Models as LLVM-to-LLVM Transformations

Authors

ŠTILL, Vladimír (203 Czech Republic, belonging to the institution), Petr ROČKAI (703 Slovakia, belonging to the institution) and Jiří BARNAT (203 Czech Republic, guarantor, belonging to the institution)

Edition

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

Publisher

Springer

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Switzerland

Confidentiality degree

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

Publication form

electronic version available online

References:

URL

Impact factor

Impact factor: 0.402 in 2005

RIV identification code

RIV/00216224:14330/16:00088094

Organization unit

Faculty of Informatics

ISBN

978-3-319-29816-0

ISSN

DOI

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

UT WoS

000374173700013

Keywords in English

memory models; model checking

Abstract

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.

Links

GA15-08772S, research and development project

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

Investor: Czech Science Foundation

Citovat

ŠTILL, Vladimír, Petr ROČKAI and 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, p. 144-155. ISBN 978-3-319-29816-0. Available from: 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 and 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, p.~144-155. ISBN~978-3-319-29816-0. Available from: https://dx.doi.org/10.1007/978-3-319-29817-7\_{}13.

Detailed Information on Publication Record