Batty, Mark and Memarian, Kayvan and Owens, Scott and Sarkar, Susmit and Sewell, Peter (2012) Clarifying and Compiling C/C++ Concurrency: From C++11 to POWER. In: POPL '12: 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 25th - 27th January, 2012, Philadelphia, USA.
| The full text of this publication is not available from this repository. (Contact us about this Publication) | |
| Official URL http://dx.doi.org/10.1145/2103656.2103717 |
Abstract
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.
| Item Type: | Conference or workshop item (Paper) |
|---|---|
| Subjects: | Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming, |
| Divisions: | Faculties > Science Technology and Medical Studies > School of Computing > Programming Languages and Systems Group |
| Depositing User: | Scott Owens |
| Date Deposited: | 24 Oct 2012 10:10 |
| Last Modified: | 18 Mar 2013 13:57 |
| Resource URI: | http://kar.kent.ac.uk/id/eprint/31893 (The current URI for this page, for reference purposes) |
- Depositors only (login required):
