[cpp-threads] C++ memory model formalisation, post-Rapperswil

[Peter Sewell]

Dear all,

we've put together a document with an introduction to our
formalisation of the C++ memory model. It includes many examples, a
description of the Cppmem tool we built for exploring the model, and a
proof of the correctness of a proposed x86 implementation, together
with a side-by-side prose and math version of the formalisation.  It's
based on the Final Committee Draft together with various changes
discussed at the Rapperswill meeting (we include some of the
motivating examples for those).  Any comments would be very welcome.

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

Mark, Scott, Susmit, Peter, and Tjark