Compiler testing via a theory of sound optimisations in the C11/C++11 memory model

Robin Morisset Pankaj Pawan Francesco Zappa Nardelli 1
1 Parkas - Parallélisme de Kahn Synchrone
DI-ENS - Département d'informatique de l'École normale supérieure, ENS Paris - École normale supérieure - Paris, Inria Paris-Rocquencourt, CNRS - Centre National de la Recherche Scientifique : UMR 8548
Abstract : 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. In this work we design a strategy to reduce the hard problem of hunting concurrency compiler bugs to differential testing of sequential code and build a tool that puts this strategy to work. Our first contribution is a theory of sound optimisations in the C11/C++11 memory model, covering most of the optimisations we have observed in real compilers and validating the claim that common compiler optimisations are sound in the C11/C++11 memory model. Our second contribution is to show how, building on this theory, concurrency compiler bugs can be identified by comparing the memory trace of compiled code against a reference memory trace for the source code. Our tool identified several mistaken write introductions and other unexpected behaviours in the latest release of the gcc compiler.
Type de document :
Communication dans un congrès
PLDI'13 - 34th ACM SIGPLAN conference on Programming language design and implementation, Jun 2013, Seattle, WA, United States. ACM, pp.187-196, 2013, 〈10.1145/2491956.2491967〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00909083
Contributeur : Francesco Zappa Nardelli <>
Soumis le : lundi 25 novembre 2013 - 17:18:14
Dernière modification le : jeudi 30 novembre 2017 - 01:17:45

Identifiants

Collections

Citation

Robin Morisset, Pankaj Pawan, Francesco Zappa Nardelli. Compiler testing via a theory of sound optimisations in the C11/C++11 memory model. PLDI'13 - 34th ACM SIGPLAN conference on Programming language design and implementation, Jun 2013, Seattle, WA, United States. ACM, pp.187-196, 2013, 〈10.1145/2491956.2491967〉. 〈hal-00909083〉

Partager

Métriques

Consultations de la notice

115