Common compiler optimisations are invalid in the C11 memory model and what we can do about it

Viktor Vafeiadis 1 Thibaut Balabonski 2 Soham Chakraborty 1 Robin Morisset 2 Francesco Zappa Nardelli 2
2 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 : We show that the weak memory model introduced by the 2011 C and C++ standards does not permit many common source-to-source program transformations (such as expression linearisation and “roach motel” reorderings) that modern compilers perform and that are deemed to be correct. As such it cannot be used to define the semantics of intermediate languages of compilers, as, for instance, LLVM aimed to. We consider a number of possible local fixes, some strengthening and some weakening the model. We evaluate the proposed fixes by determining which program transformations are valid with respect to each of the patched models. We provide formal Coq proofs of their correctness or counterexamples as appropriate.
Type de document :
Communication dans un congrès
POPL 2015 - 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Jan 2015, Mumbai, India
Liste complète des métadonnées

https://hal.inria.fr/hal-01089047
Contributeur : Francesco Zappa Nardelli <>
Soumis le : lundi 1 décembre 2014 - 08:53:46
Dernière modification le : mercredi 28 septembre 2016 - 15:51:25

Identifiants

  • HAL Id : hal-01089047, version 1

Collections

Citation

Viktor Vafeiadis, Thibaut Balabonski, Soham Chakraborty, Robin Morisset, Francesco Zappa Nardelli. Common compiler optimisations are invalid in the C11 memory model and what we can do about it. POPL 2015 - 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Jan 2015, Mumbai, India. 〈hal-01089047〉

Partager

Métriques

Consultations de la notice

264