Mathematizing C++ Concurrency

int main() {
  atomic_int x = 0;
  {{{ { x.store(1,mo_release);
        x.store(2,mo_relaxed);
        x.store(3,mo_relaxed);
        x.store(4,mo_relaxed); }
  ||| { printf("%d\n",x.load(mo_acquire).readsvalue(3) );
        x.store(5,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:

To make our semantics mathematically precise and unambigous, we express it in machine-formalised mathematics, initially in the Isabelle/HOL proof assistant and now in the Lem definition language.
To make it accessible, we introduce it with a series of examples, and give both an English-prose translation of the definitions and a typeset version of the mathematics, side-by-side; it should be possible to read either one in isolation.
To make it possible to explore the consequences of the semantics, we have developed a tool (Cppmem) that calculates the allowed executions of litmus-test example programs (using checking code automatically generated from our Lem or Isabelle/HOL definitions, for high assurance).
We discuss some issues with the N3092 draft and our proposed fixes, now incorporated into the standards.
We further validate the semantics by proving that a proposed x86 implementation of the concurrency primitives is correct with respect to the x86-TSO memory model.

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.

Papers

Mathematizing C++ Concurrency. Mark Batty, Scott Owens, Susmit Sarkar, Peter Sewell, and Tjark Weber. In POPL 2011

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.

A typeset version of the complete model, in logical order.
A Lem source of the complete model, in logical order.

People

Computer Laboratory, University of Cambridge:

[validate]