Personal tools
You are here: Home Events ICSA COLLOQUIUM TALK. Title: Making Sense of Real-world Concurrency

ICSA COLLOQUIUM TALK. Title: Making Sense of Real-world Concurrency

— filed under:

Presentation and talk by Peter Sewell, University of Cambridge. Title: Making Sense of Real-world Concurrency.

  • Colloquium Series
When Nov 10, 2011
from 03:30 PM to 04:30 PM
Where 4.31/4.33
Add event to calendar vCal


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
Document Actions