Task 2  Sample compilation of C++11 low-level atomics to Power and ARM processors

• An Axiomatic Memory Model for POWER Multiprocessors.
•    Sela Mador-Haim, Luc Maranget, Susmit Sarkar, Kayvan Memarian, Jade Alglave, Scott Owens, Rajeev Alur, Milo Martin, Peter Sewell, Derek Williams.
•    In CAV 2012.
• Synchronising C/C++ and POWER.
•    Susmit Sarkar, Kayvan Memarian, Scott Owens, Mark Batty, Peter Sewell, Luc Maranget, Jade Alglave, Derek Williams.
•    In PLDI 2012.
• Clarifying and Compiling C/C++ Concurrency: from C++11 to POWER.
•    Mark Batty, Kayvan Memarian, Scott Owens, Susmit Sarkar, and Peter Sewell.
•    In POPL 2012. (*)

• CompCertTSO: A Verified Compiler for Relaxed-Memory Concurrency.
•    Jaroslav Sevcik, Viktor Vafeiadis, Francesco Zappa Nardelli, Suresh Jagannathan, Peter Sewell.
•    In the Journal of the ACM, Volume 60 Issue 3, 2013.

• Common compiler optimisations are invalid in the C11 memory model and what we can do about it
•    V. Vafeiadis, T. Balabonsky, S. Chakraborty, R. Morisset, F. Zappa Nardelli
•    In POPL 2015.
• Compiler Testing via a Theory of Sound Optimisations in the C11/C++11 Memory Model.
•    Robin Morisset, Pankaj Pawan and Francesco Zappa Nardelli.
•    In PLDI 2013.
• Verifying Fence Elimination Optimisations.
•    Viktor Vafeiadis and Francesco Zappa Nardelli.
•    In SAS 2011. (*)

• Lem: A Lightweight Tool for Heavyweight Semantics.
•    Scott Owens, Peter Bohm, Francesco Zappa Nardelli, and Peter Sewell.
•    An ITP 2011 rough diamond. (*)