University of Cambridge > > Semantics Lunch (Computer Laboratory) > Understanding POWER Multiprocessors

Understanding POWER Multiprocessors

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Peter Sewell.

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

This talk is part of the Semantics Lunch (Computer Laboratory) series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2023, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity