BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Clarifying and Compiling C/C++ Concurrency: from C++11 to POWER - 
 Kayvan Memarian
DTSTART:20111128T124500Z
DTEND:20111128T140000Z
UID:TALK34816@talks.cam.ac.uk
CONTACT:Peter Sewell
DESCRIPTION:The upcoming C and C++ revised standards add concurrency to th
 e languages\, for the first time\, in the form of a subtle relaxed memory 
 model (the C++11 model). This aims to permit compiler optimisation and to 
 accommodate the differing relaxed-memory behaviours of mainstream multipro
 cessors\, combining simple semantics for most code with high-performance l
 ow-level atomics for concurrency libraries.\n\nIn this work\, we first est
 ablish two simpler but provably equivalent models for C/C++11\, one for th
 e full language and another for the subset without consume operations. Sub
 setting further to the fragment without low-level atomics\, we identify a 
 subtlety arising from atomic initialisation and prove that\, under an addi
 tional condition\, the model is equivalent to sequential consistency for r
 ace-free programs.\n\nWe then prove our main result\, the correctness of t
 wo proposed compilation schemes for the C/C++11 load and store concurrency
  primitives to Power assembly\, having noted that an earlier proposal was 
 flawed. (The main ideas apply also to ARM\, which has a similar relaxed me
 mory architecture.)\n\nThis should inform the ongoing development of produ
 ction compilers for C++11 and C11\, clarifies what properties of the machi
 ne architecture are required\, and builds confidence in the C/C++11 and Po
 wer semantics. \n\nJoint work with Mark Batty\, Scott Owens\, Susmit Sarka
 r\, and Peter Sewell\, to appear in POPL 2012\n
LOCATION:FW26
END:VEVENT
END:VCALENDAR