Abstract

The relaxed memory model of concurrency actually provided by today’s multiprocessors is very unclear. This is unfortunate, as understanding these models is critical for understanding and verifying real-world concurrent programs, and also for the design of high-level concurrent languages.

In this talk, I will discuss the relaxed memory model of the IBM POWER line of multiprocessors (ARM has a very similar architecture here). These provide a very subtle and highly relaxed memory model, and are widely used in highly-concurrent servers (and ARM multiprocessors have now reached commodity hardware).

Our formal model, based on extensive experiments, discussion with IBM architects, and some published detail of microarchitecture, is an abstract-machine semantics that explains many subtle examples. First presented at PLDI 2011 , we have recently extended this model to cover all the primitives used by user-level and common-case OS programmers; we can now talk of the various flavours of barriers and fancier synchronisation primitives (load-reserve and store-conditional) in a unified manner. This provides a sound basis for reasoning; an upcoming talk will discuss the correctness of compilation of C+11 concurrency on Power. Implementability on Power and ARM was a major design constraint on C+11 concurrency.

Joint work with Peter Sewell, Jade Alglave, Luc Maranget, and Derek Williams