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.
Paper
- Validating optimizations of concurrent C/C++ programs.
Soham Chakraborty, Viktor Vafeiadis.
In CGO 2016 (March 2016)
[Paper] [Slides]
Implementation
- Download our validator (packaged as a VirtualBox virtual machine): xvalidc.ova [README.txt]
People
- Soham Chakraborty, MPI-SWS
- Viktor Vafeiadis, MPI-SWS