Name
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. |
Year | DOI | Venue |
|---|---|---|
2012 | 10.1145/2103656.2103717 | POPL |
Keywords | Field | DocType |
main idea,power semantics,upcoming c,memory model,power assembly,machine architecture,provably equivalent model,store concurrency primitive,concurrency library,low-level atomics,sequential consistency,semantics | Inline function,Programming language,Concurrency,Computer science,Compatibility of C and C++,typedef,Theoretical computer science,Memory model,Return value optimization,Allocator,const | Conference |
Volume | Issue | ISSN |
47 | 1 | 0362-1340 |
Citations | PageRank | References |
50 | 1.62 | 17 |
Authors | ||
5 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Mark Batty | 1 | 203 | 9.21 |
| Kayvan Memarian | 2 | 201 | 7.84 |
| Scott Owens | 3 | 683 | 26.50 |
| Susmit Sarkar | 4 | 744 | 30.76 |
| Peter Sewell | 5 | 1446 | 68.16 |