Mathematizing C++ Concurrency

[t44-sw-out diagram]

int main() {
  atomic_int x = 0;
  {{{ {,mo_release);,mo_relaxed);,mo_relaxed);,mo_relaxed); }
  ||| { printf("%d\n",x.load(mo_acquire).readsvalue(3) );,mo_relaxed); } }}}
  return 0; }

C and C++ are defined by standards, but those standards have historically not covered the behaviour of concurrent programs, motivating an ongoing effort to specify concurrent behaviour in the recent C11 and C++11 revisions of C and C++ [WG14] [WG21, Boehm and Adve, PLDI 2008]. The key issue here is the multiprocessor relaxed-memory behaviour induced by hardware and compiler optimisations. The proposals 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 standards are prose documents: while the result of careful deliberation, the drafts were almost inevitably unclear on some points, and were subject to some subtle semantic flaws.

In this work we give a mathematically rigorous semantics for C/C++ concurrency. This and the concurrency semantics in the C/C++11 standards are in close correspondence with each other, following discussion during the standards process (some late changes have not yet been propagated into C11, but have been registered for a later Technical Corrigendum). In more detail:

We hope that this will aid discussion of any further changes to the draft standard, provide an unambiguous correctness condition for compilers, and give a basis for analysis and verification of concurrent C and C++ programs.


The Model

The model incorporates further clarifications beyond the version of POPL 2011, and also various simplified models as described in our POPL 2012 and PLDI 2012 papers. The model is now expressed in Lem, a tool for expressing lightweight executable mathematics and compiling it to LaTeX, OCaml, HOL4, and Isabelle/HOL.


Computer Laboratory, University of Cambridge:

[Mark] [Scott] [Susmit] [Peter] [Tjark]