BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Relaxed-Memory Concurrency and Verified Compilation / Mathematizin
 g C++0x concurrency - Jaroslav Sevcik and Mark Batty
DTSTART:20110117T124500Z
DTEND:20110117T140000Z
UID:TALK29243@talks.cam.ac.uk
CONTACT:Peter Sewell
DESCRIPTION:Two POPL practice talks:\n\nI will describe the semantic desig
 n and verified compilation of a\nC-like programming language for concurren
 t shared-memory computation\nabove x86 multiprocessors.  I will start with
  the correctness\nstatement\, including the surprisingly subtle design of 
 a relaxed\nx86-like memory model for a realistic subset of C. Then I will 
 outline\nour overall proof strategy\, which is largely inspired by Xavier\
 nLeroy's CompCert compiler that we build on\, with several interesting\ntw
 ists. Finally\, I will explain some of the curious subtleties\nencountered
  in the semantic design and in the proof.\n\nThis work has been done joint
 ly with Viktor Vafeiadis\, Francesco Zappa\nNardelli\, Suresh Jagannathan\
 , and Peter Sewell.\n\nThis is a practice talk for POPL 2011. It is a cut-
 down and slightly\nrevised version of my past semantics lunch talk (from 2
 2.11.2010).\n\n----------------------------------------------\n\nThe next 
 versions of C++ (C++0x) and of C (C1X) will have new concurrency\nfeatures
 \, aiming to support high-performance code with well-defined\nsemantics.  
 Unfortunately\, as we near the end of the long\nstandardization process\, 
 not all has been well.  Unsurprisingly\, the\nprose specification style of
  the draft standards is poorly suited to\ndescribe the complex design of t
 he relaxed memory model\, and in fact\nthere have been significant problem
 s.\n\nI will discuss work on formalization of the memory model\, what was\
 nbroken\, and some resulting improvements to the C++0x draft\nstandard. In
  addition I will present a tool\, Cppmem\, for graphically\nexploring the 
 semantics of small concurrent C++0x programs\, and\ndescribe a proof of th
 e correctness of a compilation strategy\ntargeting x86-TSO.\n\nThis is joi
 nt work with Scott Owens\, Susmit Sarkar\, Peter Sewell\, and\nTjark Weber
 .\n\nhttp://www.cl.cam.ac.uk/~pes20/cpp/\n
LOCATION:Room FW26\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR