Skip to main content

Mathematizing C++ concurrency

Batty, Mark and Owens, Scott and Sarkar, Susmit and Sewell, Peter and Weber, Tjark (2011) Mathematizing C++ concurrency. In: Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages. ACM, New York, USA, pp. 55-66. ISBN 978-1-4503-0490-0. (doi:10.1145/1926385.1926394) (KAR id:50265)

PDF Pre-print
Language: English
Download (318kB) Preview
[thumbnail of popl085ap-sewell.pdf]
This file may not be suitable for users of assistive technology.
Request an accessible format
Official URL:


Shared-memory concurrency in C and C++ is pervasive in systems programming, but has long been poorly defined. This motivated an ongoing shared effort by the standards committees to specify concurrent behaviour in the next versions of both languages. They aim to provide strong guarantees for race-free programs, together with new (but subtle) relaxed-memory atomic primitives for high-performance concurrent code. However, the current draft standards, while the result of careful deliberation, are not yet clear and rigorous definitions, and harbour substantial problems in their details.

In this paper we establish a mathematical (yet readable) semantics for C++ concurrency. We aim to capture the intent of the current (`Final Committee') Draft as closely as possible, but discuss changes that fix many of its problems. We prove that a proposed x86 implementation of the concurrency primitives is correct with respect to the x86-TSO model, and describe our Cppmem tool for exploring the semantics of examples, using code generated from our Isabelle/HOL definitions.

Having already motivated changes to the draft standard, this work will aid discussion of any further changes, provide a correctness condition for compilers, and give a much-needed basis for analysis and verification of concurrent C and C++ programs.

Item Type: Book section
DOI/Identification number: 10.1145/1926385.1926394
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)
Batty, Mark:
Owens, Scott:
  • Depositors only (login required):


Downloads per month over past year