Skip to content

Research at St Andrews

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

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Author(s)

Mark Batty, Kayvan Memarian, Scott Owens, Susmit Sarkar, Peter Sewell

School/Research organisations

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.

Close

Details

Original languageEnglish
Title of host publicationPOPL 12: PROCEEDINGS OF THE 39TH ANNUAL ACM SIGPLAN-SIGACT SYMPOSIUM ON PRINCIPLES OF PROGRAMMING LANGUAGES
Place of PublicationNEW YORK
PublisherASSOC COMPUTING MACHINERY
Pages509-520
Number of pages12
ISBN (Print)978-1-4503-1083-3
StatePublished - 2012
Event39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages - Philadelphia, Panama
Duration: 25 Jan 201227 Jan 2012

Conference

Conference39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
CountryPanama
CityPhiladelphia
Period25/01/1227/01/12

    Research areas

  • PROGRAMS, Relaxed Memory Models, Semantics

Discover related content
Find related publications, people, projects and more using interactive charts.

View graph of relations

Related by author

  1. Memory consistency models using constraints

    Akgün, Ö., Hoffmann, R. & Sarkar, S. 27 Aug 2018 The Seventeenth Workshop on Constraint Modelling and Reformulation (ModRef 2018), Proceedings. 16 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  2. Automatically deriving cost models for structured parallel processes using hylomorphisms

    Castro, D., Hammond, K., Sarkar, S. & Alguwaifli, Y. Feb 2018 In : Future Generation Computer Systems. 79, Part 2, p. 653-668

    Research output: Contribution to journalArticle

  3. Simplifying ARM concurrency: multicopy-atomic axiomatic and operational models for ARMv8

    Pulte, C., Flur, S., Deacon, W., French, J., Sarkar, S. & Sewell, P. Jan 2018 Proceedings of the ACM on Programming Languages (POPL '18). New York: ACM, Vol. 2 Issue POPL, 29 p. 19

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  4. Verification of a lazy cache coherence protocol against a weak memory model

    Banks, C., Elver, M., Hoffmann, R., Sarkar, S., Jackson, P. & Nagarajan, V. 2 Oct 2017 Proceedings of the 17th Conference on Formal Methods in Computer-Aided Design (FMCAD). ACM, p. 60-67

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  5. Mixed-size Concurrency: ARM, POWER, C/C++11, and SC

    Flur, S., Sarkar, S., Pulte, C., Nienhuis, K., Maranget, L., Gray, K., Sezgin, A., Batty, M. & Sewell, P. 1 Jan 2017 Proceedings of the 44th annual ACM-SIGPLAN Symposium on Principles of programming languages. ACM, p. 429-442

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

ID: 44375816