Skip to main content

Synchronising C/C++ and POWER

Sarkar, Susmit and Memarian, Kayvan and Owens, Scott and Batty, Mark and Sewell, Peter and Maranget, Luc and Alglave, Jade and Williams, Derek (2012) Synchronising C/C++ and POWER. In: Proceedings of the 33rd ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM, New York, USA, pp. 311-322. ISBN 978-1-4503-1205-9. (doi:10.1145/2254064.2254102) (KAR id:50269)

Language: English
Download (241kB) Preview
[thumbnail of pldi010-sarkar.pdf]
This file may not be suitable for users of assistive technology.
Request an accessible format
Official URL:


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®, POWER®, 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.

Item Type: Book section
DOI/Identification number: 10.1145/2254064.2254102
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 75 Electronic computers. Computer science
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Mark Batty
Date Deposited: 03 Nov 2015 08:27 UTC
Last Modified: 16 Nov 2021 10:20 UTC
Resource URI: (The current URI for this page, for reference purposes)
Owens, Scott:
Batty, Mark:
  • Depositors only (login required):


Downloads per month over past year