Reasoning about C11 Program Transformations
Introduction
We show that the weak memory model introduced by the 2011 C and C++ standards does not permit many of common sourcetosource program transformations (such as expression linearisation and "roach motel" reordering) 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.
Papers

Viktor Vafeiadis, Thibaut Balabonski, Soham Chakraborty, Robin Morisset, and Francesco Zappa Nardelli.
Common compiler optimisations are invalid in the C11 memory model and what we can do about it.
In POPL 2015: 42nd ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, ACM, 2015.
Slides
 Reasoning about the C/C++ weak memory model, Invited talk at EC2/REORDER, given on 20140717 at Vienna. (This talk also covers some material that is not part of this work.)
 'Easy' fixes to the C11 memory model, Talk given on 20140925 at Cambridge, UK.
Coq formalisation
 Download the formalization [c11comp1.0.zip, 81KB] [README.txt] [CHANGELOG.txt] [all versions]
 Browse the formalization online [proofs hidden] [proofs visible]
People
 Viktor Vafeiadis (MPISWS)
 Thibaut Balabonski (INRIA)
 Soham Chakraborty (MPISWS)
 Robin Morisset (INRIA)
 Francesco Zappa Nardelli (INRIA)