Mathematizing C++ Concurrency: The Post-Rapperswil Model
Mark Batty, Scott Owens, Susmit Sarkar, Peter Sewell, Tjark Weber · Kent Academic Repository (University of Kent) · 2010
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.