Weak Memory Models as LLVM-to-LLVM Transformations

Logo poskytovatele

Varování

Publikace nespadá pod Pedagogickou fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.
Autoři

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

Rok publikování 2016
Druh Článek ve sborníku
Konference Mathematical and Engineering Methods in Computer Science - 10th International Doctoral Workshop
Fakulta / Pracoviště MU

Fakulta informatiky

Citace
www http://dx.doi.org/10.1007/978-3-319-29817-7_13
Doi http://dx.doi.org/10.1007/978-3-319-29817-7_13
Obor Informatika
Klíčová slova memory models; model checking
Popis 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.
Související projekty:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.