cmmtest
Hunting Concurrency Compiler Bugs

Compilers sometimes generate correct sequential code but break the concurrency memory model of the programming language: these subtle compiler bugs are observable only when the miscompiled functions interact with concurrent contexts, making them particularly hard to detect. The cmmtest tool performs differential testing to hunt concurrency compiler bugs in C and C++ compilers against the C11/C++11 memory model. The tool is still under development but it already identified several mistaken write introductions and other unexpected behaviours in the latest release of the gcc compiler.

Resources:

  • Cmmtest in a nutshell [.pdf];
  • Compiler Testing via a Theory of Sound Optimisations in the C11/C++11 Memory Model, in PLDI'13 [.pdf];
  • a document with detailed proofs of the theorems in the paper;
  • the list of gcc bugs / unexpected behaviours reported.

    The release 0.2 of cmmtest can be downloaded here. An incomplete readme is also available.

    Please contact Francesco Zappa Nardelli for problems with the installation procedure or doubts about the use of the tool.

    People:

  • Robin Morisset
  • Pankaj Pawan
  • Francesco Zappa Nardelli

    • with contributions of Anirudh Kumar, Pankaj More and Pankaj Prateek.

    Last update: