Validating optimizations of concurrent C/C++ programs

4 years 3 months ago
Validating optimizations of concurrent C/C++ programs
We present a validator for checking the correctness of LLVM compiler optimizations on C11 programs as far as concurrency is concerned. Our validator checks that optimizations do not change memory accesses in ways disallowed by the C11 and/or LLVM memory models. We use a custom C11 concurrent program generator to trigger multiple LLVM optimizations and evaluate the efficacy of our validator. Our experiments highlighted the difference between the C11 and LLVM memory models, and uncovered a number of previously unknown compilation errors in the LLVM optimizations involving the C11 concurrency primitives. Categories and Subject Descriptors D.2.4 [Software Engineering]: Software/Program Verification; D.3.4 [Programming Languages]: Processors; F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs Keywords Concurrency; Weak Memory Models; C/C++; LLVM; Translation Validation
Soham Chakraborty, Viktor Vafeiadis
Added 31 Mar 2016
Updated 31 Mar 2016
Type Journal
Year 2016
Where CGO
Authors Soham Chakraborty, Viktor Vafeiadis
Comments (0)