BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.cam.ac.uk//v3//EN
BEGIN:VTIMEZONE
TZID:Europe/London
BEGIN:DAYLIGHT
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
TZNAME:BST
DTSTART:19700329T010000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
TZNAME:GMT
DTSTART:19701025T020000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
CATEGORIES:Logic and Semantics Seminar (Computer Laboratory)
SUMMARY:Modular Relaxed Dependencies in Weak Memory Concur
 rency - Marco Paviotti
DTSTART;TZID=Europe/London:20191205T140000
DTEND;TZID=Europe/London:20191205T150000
UID:TALK135556AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/135556
DESCRIPTION:We present a denotational semantics for weak memor
 y concurrency that avoids thin-air reads\, provide
 s data-race free programs with sequentially consis
 tent semantics (DRF-SC)\, and supports a compositi
 onal refinement relation for validating optimisati
 ons.\nWe then use this semantics to fix the C++ me
 mory model\, which we call RD-C11 (Relaxed Depende
 ncies C11). We show RD-C11 is the first C++ model 
 the avoids thin-air reads that is aligned with the
  axiomatic-style specification of the ISO standard
 \, provides the DRF-SC property\, is efficiently i
 mplementable over hardware architectures and that 
 is tested via a simulator over a battery of litmus
  tests.
LOCATION:Computer Laboratory\, Room FW11
CONTACT:Jean Pichon-Pharabod
END:VEVENT
END:VCALENDAR