The upcoming C and C++ revised standards add concurrency to the languages, for the first time, in the form of a subtle *relaxed memory model* (the *C++11 model*). This aims to permit compiler optimisation and to accommodate the differing relaxed-memory behaviours of mainstream multiprocessors, combining simple semantics for most code with high-performance *low-level atomics* for concurrency libraries.

In this paper, we first establish two simpler but provably equivalent models for C++11, one for the full language and another for the subset without consume operations. Subsetting further to the fragment without low-level atomics, we identify a subtlety arising from atomic initialisation and prove that, under an additional condition, the model is equivalent to sequential consistency for race-free programs.

We then prove our main result, the correctness of two proposed compilation schemes for the C++11 load and store concurrency primitives to Power assembly, having noted that an earlier proposal was flawed. (The main ideas apply also to ARM, which has a similar relaxed memory architecture.)

This should inform the ongoing development of production compilers for C++11 and C1x, clarifies what properties of the machine architecture are required, and builds confidence in the C++11 and Power semantics.

- 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.

The models are expressed in Lem code, a lightweight language for executable mathematical definitions.

`MachineDefUtils.lem``MachineDefFreshIds.lem``MachineDefValue.lem``MachineDefTypes.lem``MachineDefInstructionSemantics.lem``MachineDefStorageSubsystem.lem``MachineDefThreadSubsystem.lem``MachineDefSystem.lem`

`atomic_theorems.sml`The HOL4 results of Section 3, and hand proofs supporting Lemma 4.3:`atomic_simple.lem`Simplifying the C++11 model to the fragment treated in the second half of the paper`intermediate_actions.lem`Defining a type of “intermediate actions”, to relate C++11 actions and POWER trace events`statement.lem`The main correctness statement of compilation, as described in Section 7.1`power_thread_lemmas.lem`Key properties of the POWER thread semantics used extensively in the proofs below`build_sc_order.lem`We can always build a linear SC order from the POWER trace with properties necessary for a C++11 SC order, as described in Section 7.3`power_to_consistent_ex.lem`Analysis of a POWER trace with respect to derived C++11 relations, as described in Section 7.2; and a proof that (assuming an “rf in hb” condition) a POWER trace can always be related to a consistent C++11 execution witness, as described in Section 7.4`c_add_read.lem`Lemmas about adding reads to a partial C++11 execution, necessary for the proof described in Section 7.5`proof.lem`The top level of the proof, using the preceding results

University of Cambridge:

INRIA Paris-Rocquencourt: