Mark Batty, Scott Owens, Susmit Sarkar, Peter Sewell, and Tjark Weber. Technical Report N3132, ISO IEC JTC1/SC22/WG21, August 2010. http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2010/n3132.pdf.
In this paper we describe a rigorous semantics for C++ concurrency. To the best of our knowledge, this captures the intent of the Final Committee Draft (N3092) text, modified as discussed at the Rapperswil meeting of the C++ Standards Committee in July 2010. We discuss some issues with the N3092 text that led to those changes.
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 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 much-needed basis for analysis and verification of concurrent C and C++ programs.
@techreport{batty10mathematizing,
author = {Mark Batty and Scott Owens and Susmit Sarkar and Peter Sewell and Tjark Weber},
title = {Mathematizing {C++} Concurrency: The Post-{Rapperswil} Model},
institution = {ISO IEC JTC1/SC22/WG21},
number = {N3132},
month = aug,
year = {2010},
note = {\url{http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2010/n3132.pdf}}
}