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 - Jaroslav Sev
 cik
DTSTART:20101122T124500Z
DTEND:20101122T140000Z
UID:TALK27336@talks.cam.ac.uk
CONTACT:Sam Staton
DESCRIPTION:I will describe the semantic design and verified compilation o
 f a C-like programming language for concurrent shared-memory computation a
 bove x86 multiprocessors.  I will start with the correctness statement\, i
 ncluding the surprisingly subtle design of a relaxed x86-like memory model
  for a realistic subset of C. Then I will outline our overall proof strate
 gy\, which is largely inspired by Xavier Leroy's CompCert compiler that we
  build on\, with several interesting twists. Finally\, I will explain some
  of the curious subtleties\nencountered in the semantic design and in the 
 proof.\n\nThis is joint work with Viktor Vafeiadis\, Francesco Zappa Narde
 lli\, Suresh Jagannathan\, and Peter Sewell.\n
LOCATION:Room FW26\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR