Making Sense of Real-world Concurrency
- 16:30 29th November 2011 ( week 8, Michaelmas Term 2011 )Lecture Theatre B
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
Speaker bio
Peter Sewell is a Reader in Computer Science and EPSRC Leadership Fellow at the University of Cambridge Computer Laboratory. He studied at Cambridge, Oxford, and Edinburgh, taking his PhD, supervised by Robin Milner, in 1995. With a background in concurrency theory and programming language semantics, his research now is directed towards putting the engineering of real-world computer systems on solid foundations, developing techniques (at once mathematically rigorous and pragmatically useful) to enable the construction of systems that are better-understood, more robust, and more secure. This applied semantics work has involved programming languages, network protocols, and security, and currently is focussed on the relaxed memory models of multiprocessors and concurrent languages.Share this:
