[cpp-threads] CompCertTSO release, verified optimisations, POWER memory model

[Jaroslav Sevcik]

Readers of this list might be interested in the following recent work
from our group:

a) our recent release of CompCertTSO, a certified compiler from a
multithreaded C-like language with a TSO relaxed memory model to x86
assembly language with a realistic x86-TSO memory model; the
development builds on CompCert.  This includes some verified fence
elimination optimisations. The code, documentation, and papers
are available here:
http://www.cl.cam.ac.uk/~pes20/CompCertTSO/

b) work on Safe Optimisations for Shared-Memory Concurrent Programs:
http://www.cl.cam.ac.uk/~js861/papers/transsafety.pdf

c) a formal and experimentally validated operational memory model for
POWER multiprocessors:
http://www.cl.cam.ac.uk/~pes20/ppc-supplemental/index.html

Any comments would be very welcome.

Jaroslav (for the authors of all three)