Séminaires des équipes de recherche
Sound Optimisations in the C11/C++11 Memory Model and Applications to Compiler Testing
- Date : 8/10/2012
- Place : Inria - Rocquencourt - Amphithéâtre Alan Turing
- Guest(s) : Francesco Zappa Nardelli
- Organiser(s) : Gallium - Moscova
Sometimes compilers introduce bugs: the generated code allows behaviours forbidden by the semantics of the source program. Most of the time these misbehaviours materialise as soon as the code is executed. However, in some subtle cases, the compiler generates perfect sequential code but breaks the memory model of the programming language: unexpected behaviours become observable only when the miscompiled function interacts with a concurrent context. We call
these concurrency compiler bugs. In this work we present cpptest, a tool for hunting concurrency compiler bugs in modern C and C++ compilers. First we prove correct a theory of sound optimisations in the C11/C++11 memory model, covering most of the optimisations we have observed testing real compilers (including eliminations, reorderings and a restricted class of introductions of memory accesses). Building on this theory, we show how concurrency compiler bugs can be
identified by comparing the memory trace of compiled code against a reference memory trace for the source code: this effectively reduces
the hard problem of hunting concurrency compilation bugs to differential testing of sequential code. The cpptest tool puts this idea at work: at the time of writing, preliminary testing of gcc and clang has already identified some mistaken write introduction performed by the loop invariant motion optimisation in gcc 4.7.
This is work in progress with Robin Morisset and Pankaj Pawan.