Clarifying and Compiling C/C++ Concurrency: from C++11 to POWER

Add to your list(s) Download to your calendar using vCal

• Kayvan Memarian
• Monday 28 November 2011, 12:45-14:00
• FW26.

If you have a question about this talk, please contact Peter Sewell.

This talk has been canceled/deleted

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 work, we first establish two simpler but provably equivalent models for C/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/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 C11 , clarifies what properties of the machine architecture are required, and builds confidence in the C/C+11 and Power semantics.

Joint work with Mark Batty, Scott Owens, Susmit Sarkar, and Peter Sewell, to appear in POPL 2012

This talk is part of the Semantics Lunch (Computer Laboratory) series.

This talk is included in these lists:

This talk is not included in any other list

Note that ex-directory lists are not shown.