Weak Memory Models as LLVM-to-LLVM Transformations

March 3, 2020

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.

Authors: Vladimír ŠtillPetr Ročkai, and Jiří Barnat

Project: DIVINE4

Published in: Mathematical and Engineering Methods in Computer Science, Revised Selected Papers, Springer International Publishing, 2016, volume 9548 of Lecture Notes in Computer Science, 144–155.

Go to pdf

Article Link

Authors

Partner University

Collaborations

Institutes

Associated Research Projects