Skip to content

Research at St Andrews

Synchronising C/C plus plus and POWER

Research output: Contribution to journalArticle

DOI

Author(s)

Susmit Sarkar, Kayvan Memarian, Scott Owens, Mark Batty, Peter Sewell, Luc Maranget, Jade Alglave, Derek Williams

School/Research organisations

Abstract

Shared memory concurrency relies on synchronisation primitives: compare-and-swap, load-reserve/store-conditional (aka LL/SC), language-level mutexes, and so on. In a sequentially consistent setting, or even in the TSO setting of x86 and Sparc, these have well-understood semantics. But in the very relaxed settings of IBM (R) POWER (R), ARM, or C/C++, it remains surprisingly unclear exactly what the programmer can depend on.

This paper studies relaxed-memory synchronisation. On the hardware side, we give a clear semantic characterisation of the load-reserve/store-conditional primitives as provided by POWER multiprocessors, for the first time since they were introduced 20 years ago; we cover their interaction with relaxed loads, stores, barriers, and dependencies. Our model, while not officially sanctioned by the vendor, is validated by extensive testing, comparing actual implementation behaviour against an oracle generated from the model, and by detailed discussion with IBM staff. We believe the ARM semantics to be similar.

On the software side, we prove sound a proposed compilation scheme of the C/C++ synchronisation constructs to POWER, including C/C++ spinlock mutexes, fences, and read-modify-write operations, together with the simpler atomic operations for which soundness is already known from our previous work; this is a first step in verifying concurrent algorithms that use load-reserve/store-conditional with respect to a realistic semantics. We also build confidence in the C/C++ model in its own terms, fixing some omissions and contributing to the C standards committee adoption of the C++11 concurrency model.

Close

Details

Original languageEnglish
Pages (from-to)311-321
Number of pages11
JournalACM SIGPLAN Notices
Volume47
Issue number6
DOIs
StatePublished - Jun 2012

    Research areas

  • PROGRAMS, Relaxed Memory Models, MEMORY, Reliability, Verification, Standardisation, Semantics, Theory, Languages

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

Related by journal

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

    Batty, M., Memarian, K., Owens, S., Sarkar, S. & Sewell, P. Jan 2012 In : ACM SIGPLAN Notices. 47, 1, p. 509-520 12 p.

    Research output: Contribution to journalArticle

  2. Mathematizing C++ Concurrency

    Batty, M., Owens, S., Sarkar, S., Sewell, P. & Weber, T. Jan 2011 In : ACM SIGPLAN Notices. 46, 1, p. 55-66 12 p.

    Research output: Contribution to journalArticle

  3. Understanding POWER Multiprocessors

    Sarkar, S., Sewell, P., Alglave, J., Maranget, L. & Williams, D. Jun 2011 In : ACM SIGPLAN Notices. 46, 6, p. 175-186 12 p.

    Research output: Contribution to journalArticle

  4. The Semantics of x86-CC Multiprocessor Machine Code

    Sarkar, S., Sewell, P., Nardelli, F. Z., Owens, S., Ridge, T., Braibant, T., Myreen, M. O. & Alglave, J. Jan 2009 In : ACM SIGPLAN Notices. 44, 1, p. 379-391 13 p.

    Research output: Contribution to journalArticle

ID: 44375728