Mathematizing C plus plus Concurrency

Mark Batty*, Scott Owens, Susmit Sarkar, Peter Sewell, Tjark Weber

*Corresponding author for this work

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

Abstract

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 :ode. 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 he 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.

Original languageEnglish
Title of host publicationPOPL 11: PROCEEDINGS OF THE 38TH ANNUAL ACM SIGPLAN-SIGACT SYMPOSIUM ON PRINCIPLES OF PROGRAMMING LANGUAGES
Place of PublicationNEW YORK
PublisherACM
Pages55-66
Number of pages12
ISBN (Print)978-1-4503-0490-0
Publication statusPublished - 2011
Event38th Symposium on Principles of Programming Languages - Austin
Duration: 26 Jan 201128 Jan 2011

Conference

Conference38th Symposium on Principles of Programming Languages
CityAustin
Period26/01/1128/01/11

Keywords

  • Relaxed Memory Models
  • Semantics

Fingerprint

Dive into the research topics of 'Mathematizing C plus plus Concurrency'. Together they form a unique fingerprint.

Cite this