Making Sense of Real-world Concurrency
Since 2007, my colleagues and I have been trying to make sense of shared-memory concurrency as it exists in mainstream systems, looking especially at x86, IBM Power, and ARM multiprocessors, and at the forthcoming C11 and C++11 standards. These systems do not have the simple sequentially consistent behaviour that has been assumed in almost all work on semantics and verification; instead, they exhibit subtle relaxed memory models that arise from hardware and compiler optimisations, and these are often poorly specified.
We have built mathematically rigorous models for the x86, Power and C/C++ concurrency behaviour, validated by extensive experimental testing and discussion with the designers. Above these, we have proved correctness (mechanised in Coq) of a compiler from a concurrent C-like language to x86 (CompCertTSO) and correctness of compilation schemes from the C/C++ concurrency primitives to those of Power (ARM is similar). I'll talk about some of this experience, focussing especially on our Power/ARM rigorous architectural specification, compilation of C/C++11 to that, and current work on synchronisation primitives.
This is joint work with Mark Batty, Kayvan Memarian, Magnus Myreen, Scott Owens, Tom Ridge, Susmit Sarkar, and Jaroslav Sevcik (University of Cambridge); Luc Maranget and Francesco Zappa Nardelli (INRIA); Jade Alglave (Oxford University); Suresh Jagannathan (Purdue University); Viktor Vafeiadis (MPI-SWS Saarbrucken); and Derek Williams (IBM Austin).
Further details are available at http://www.cl.cam.ac.uk/~pes20/weakmemory