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 a forthcoming revision of C++ (unofficially, C++0x) [WG21, Boehm and Adve, PLDI 2008]. The next C standard (unofficially, C1X) [WG14] is expected to follow suit. 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 draft standards (e.g. the Final Committee Draft (N3092), are prose documents: while the result of careful deliberation, they are almost inevitably unclear on some points, and are subject to some subtle semantic flaws.
In this work we give a mathematically rigorous semantics for C++ concurrency. To the best of our knowledge, this captures the intent of the Final Committee Draft (N3092) text, modified to incorporate changes we suggested at the Rapperswil meeting of the C++ Standards Committee in July 2010. In more detail:
- To make our semantics mathematically precise and unambigous, we express it in machine-formalised mathematics, in the Isabelle/HOL proof assistant.
- 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 Isabelle/HOL definitions, for high assurance).
- We discuss some issues with the N3092 draft and our proposed fixes.
- 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
Mathematizing C++ Concurrency: The Post-Rapperswil Model. September 1, 2010. (This is a revision of C++ Standards Committee Paper N3132=10-0122. August 23, 2010) Mark Batty, Scott Owens, Susmit Sarkar, Peter Sewell, and Tjark Weber.
The Model
- A typeset version of the complete model, in logical order.
- The Isabelle/HOL script for the definitions of the model: Atomic.thy.
These relate to the pre-Rapperswil version of the model. The post-Rapperswil model, and the changes, are described in N3132 and the paper above.
Proofs
Examples
- See the Post-Rapperswil paper above
People
Computer Laboratory, University of Cambridge:
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; }