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

Robin Morisset 1 Pankaj Pawan 2, 1 Francesco Zappa Nardelli 1
1 Parkas - Parallélisme de Kahn Synchrone
DI-ENS - Département d'informatique de l'École normale supérieure, 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 2013 - 34th ACM SIGPLAN conference on Programming language design and implementation, Jun 2013, Seattle, WA, United States. ACM, PLDI '13 Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation, 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 : dimanche 22 juillet 2018 - 09:10:03

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 2013 - 34th ACM SIGPLAN conference on Programming language design and implementation, Jun 2013, Seattle, WA, United States. ACM, PLDI '13 Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp.187-196, 2013, 〈10.1145/2491956.2491967〉. 〈hal-00909083〉

Partager

Métriques

Consultations de la notice

179