BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Mathematizing C++ Concurrency - Mark Batty (University of Cambridg
 e)
DTSTART:20101018T114500Z
DTEND:20101018T130000Z
UID:TALK26712@talks.cam.ac.uk
CONTACT:Sam Staton
DESCRIPTION:New versions of C++ (C++0x) and of C (C1X) will have new concu
 rrency features\,\naiming to support high-performance code with well-defin
 ed semantics. Unfortunately\,\nas we near the end of the long standardizat
 ion process\, not all has been\nwell. Unsurprisingly\, the prose specifica
 tion style of the draft standards\nis poorly suited to describe the comple
 x design of the relaxed memory model\,\nand in fact there have been signif
 icant problems.\n\nI will discuss work on formalization of the memory mode
 l\, what was broken\,\nand some resulting improvements to the C++0x draft 
 standard. In addition\nI will present a tool\, Cppmem\, for graphically ex
 ploring the semantics of\nsmall concurrent C++0x programs\, and describe a
  proof of the correctness\nof a compilation strategy targeting x86-TSO.\n\
 nThis is joint work with Scott Owens\, Susmit Sarkar\, Peter Sewell\, and 
 Tjark\nWeber.
LOCATION:Room FW26\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR