Common compiler optimisations are invalid in the C11 memory model and what we can do about it
In: POPL 2015-42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages POPL 2015-42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Jan 2015, Mumbai, India POPL; (2015-01-15)
Online
unknown
Zugriff:
International audience; 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.
| Titel: |
Common compiler optimisations are invalid in the C11 memory model and what we can do about it
|
|---|---|
| Autor/in / Beteiligte Person: | Francesco Zappa Nardelli ; Morisset, Robin ; Chakraborty, Soham ; Vafeiadis, Viktor ; Balabonski, Thibaut ; Max Planck Institute for Software Systems (MPI-SWS) ; Parallélisme de Kahn Synchrone (Parkas ) ; Centre National de la Recherche Scientifique (CNRS)-Inria Paris-Rocquencourt ; Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Département d'informatique de l'École normale supérieure (DI-ENS) ; École normale supérieure - Paris (ENS Paris) ; Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Paris (ENS Paris) ; Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Centre National de la Recherche Scientifique (CNRS) ; Département d'informatique - ENS Paris (DI-ENS) ; École normale supérieure - Paris (ENS-PSL) ; Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Paris (ENS-PSL) ; Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Inria Paris-Rocquencourt ; Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS) ; Zappa Nardelli, Francesco ; Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-École normale supérieure - Paris (ENS Paris) ; Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-École normale supérieure - Paris (ENS Paris) ; Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Inria Paris-Rocquencourt |
| Link: | |
| Quelle: | POPL 2015-42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages POPL 2015-42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Jan 2015, Mumbai, India POPL; (2015-01-15) |
| Veröffentlichung: | HAL CCSD, 2015 |
| Medientyp: | unknown |
| Schlagwort: |
|
| Sonstiges: |
|