[cpp-threads] C++ memory model

[Mark Batty]

Dear all,

I've been looking at the memory model described in the draft C++
standard, N2914, trying to understand the model mathematically and
(ultimately) to provide a basis for C++ metatheory and program or
compiler verification.

Currently, I've formalized a subset of the model without
non-sequentially-consistent low-level atomics, and have a
machine-checked proof that for any race-free execution there exists a
sequentially consistent execution with the same memory actions (along
the lines of Theorem 7.1 of Boehm and Adve's PLDI 2008 paper).

In the process of this formalization and proof some parts of the draft
standard seemed difficult to understand or inconsistent - mostly
relatively local points.  I've written a note describing the
formalization and some specific suggestions for local clarifications
and improvements to the standard.  There's a copy here:

 http://www.cl.cam.ac.uk/~mjb220/cpp/cpp.pdf

I would welcome any comments you have.  Please feel free to forward
that url to anyone else who might be interested.

Mark