COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. |
University of Cambridge > Talks.cam > Semantics Lunch (Computer Laboratory) > Understanding POWER Multiprocessors
Understanding POWER MultiprocessorsAdd 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. This talk is included in these lists:
Note that ex-directory lists are not shown. |
Other listsBeyond Profit Trinity Hall History Society Clare Hall TalksOther talks"Mechanosensitive regulation of cancer epigenetics and pluripotency" EMERGING EPIGENETICS: DETECTING & MODIFYING EPIGENETICS MARKS UK 7T travelling-head study: pilot results Visual Analytics for High-Dimensional Data Exploration and Engineering Design In search of amethysts, black gold and yellow gold CANCELLED IN SYMPATHY WITH STRIKE Nationality, Alienage and Early International Rights Structural basis for human mitochondrial DNA replication, repair and antiviral drug toxicity Amino acid sensing: the elF2a signalling in the control of biological functions 'The Japanese Mingei Movement and the art of Katazome' 100 Problems around Scalar Curvature Uncertainty Quantification of geochemical and mechanical compaction in layered sedimentary basins |