Weak Memory Models as LLVM-to-LLVM Transformations

Investor logo

Warning

This publication doesn't include Faculty of Arts. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

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

Year of publication 2016
Type Article in Proceedings
Conference Mathematical and Engineering Methods in Computer Science - 10th International Doctoral Workshop
MU Faculty or unit

Faculty of Informatics

Citation
Web 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
Field Informatics
Keywords memory models; model checking
Description 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.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.