ŠTILL, Vladimír, Petr ROČKAI a Jiří BARNAT. Weak Memory Models as LLVM-to-LLVM Transformations. In Jan Kofroň and Tomáš Vojnar. Mathematical and Engineering Methods in Computer Science - 10th International Doctoral Workshop. Neuveden: Springer, 2016. s. 144-155, 12 s. ISBN 978-3-319-29816-0. doi:10.1007/978-3-319-29817-7_13.
Další formáty:   BibTeX LaTeX RIS
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
Originální 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"
WWW 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 0302-9743
Doi http://dx.doi.org/10.1007/978-3-319-29817-7_13
Klíčová slova anglicky memory models; model checking
Příznaky Mezinárodní význam, Recenzováno
Změnil Změnil: RNDr. Pavel Šmerk, Ph.D., učo 3880. Změněno: 27. 4. 2017 11:33.
Anotace
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 VaVNázev: Analýza korektnosti vícevláknových programů v C a C++
Investor: Grantová agentura ČR, Standardní projekty
VytisknoutZobrazeno: 20. 1. 2020 18:29