Sciweavers

POPL
2015
ACM

Common Compiler Optimisations are Invalid in the C11 Memory Model and what we can do about it

7 years 11 months ago
Common Compiler Optimisations are Invalid in the C11 Memory Model and what we can do about it
We show that the weak memory model introduced by the 2011 C and C++ standards does not permit many common source-tosource 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. Categories and Subject Descriptors D.3.1 [Programming Languages]: Formal Definitions and Theory; D.3.3 [Programming Languages]: Language Constructs and Features Keywords Concurrency; Weak memory models; C/C++; Compilers; Program transformations
Viktor Vafeiadis, Thibaut Balabonski, Soham Chakra
Added 16 Apr 2016
Updated 16 Apr 2016
Type Journal
Year 2015
Where POPL
Authors Viktor Vafeiadis, Thibaut Balabonski, Soham Chakraborty, Robin Morisset, Francesco Zappa Nardelli
Comments (0)