BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Understanding POWER Multiprocessors - Susmit Sarkar
DTSTART:20111114T124500Z
DTEND:20111114T140000Z
UID:TALK33918@talks.cam.ac.uk
CONTACT:Peter Sewell
DESCRIPTION:The relaxed memory model of concurrency actually provided by t
 oday's multiprocessors is very unclear. This is unfortunate\, as understan
 ding these models is critical for understanding and verifying real-world c
 oncurrent programs\, and also for the design of high-level concurrent lang
 uages.\n\nIn this talk\, I will discuss the relaxed memory model of the IB
 M POWER line of multiprocessors (ARM has a very similar architecture here)
 . These provide a very subtle and highly relaxed memory model\, and are wi
 dely used in highly-concurrent servers (and ARM multiprocessors have now r
 eached commodity hardware).\n\nOur formal model\, based on extensive exper
 iments\, discussion with IBM architects\, and some published detail of mic
 roarchitecture\, is an abstract-machine semantics that explains many subtl
 e examples. First presented at PLDI 2011\, we have recently extended\nthis
  model to cover all the primitives used by user-level and common-case OS p
 rogrammers\; we can now talk of the various flavours of barriers and fanci
 er synchronisation primitives (load-reserve and store-conditional) in a un
 ified 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++1
 1 concurrency.\n\nJoint work with Peter Sewell\, Jade Alglave\, Luc Marang
 et\, and Derek Williams
LOCATION:FW26
END:VEVENT
END:VCALENDAR