BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Library Abstraction for C/C++ Concurrency - Mark Batty
DTSTART:20121203T130000Z
DTEND:20121203T140000Z
UID:TALK41247@talks.cam.ac.uk
CONTACT:Peter Sewell
DESCRIPTION:When constructing complex concurrent systems\, abstraction is 
 vital: programmers should be able to reason about concurrent libraries in 
 terms of abstract specifications that hide the implementation details.  Re
 laxed memory models present substantial challenges in this respect\, as li
 braries need not provide sequentially consistent abstractions: to avoid un
 necessary synchronisation\, they may allow clients to observe relaxed memo
 ry effects\, and library specifications must capture these.\n\nThis talk d
 escribes a criterion for sound library abstraction in the new C11 memory m
 odel\, generalising the standard sequentially consistent notion of lineari
 zability. We have proved that our criterion soundly captures all client-li
 brary interactions\, both through call and return values\, and through the
  subtle synchronisation effects arising from the memory model. To illustra
 te the approach\, a specification and verified implementation of the lock-
 free Treiber stack will be described. Ours is the first approach to compos
 itional reasoning for concurrent C11 programs.\n\nThis is joint work with 
 Mike Dodds and Alexey Gotsman.\n\nThis is a POPL practice talk\, so should
  fit into a 30 minute slot.  Comments are welcome!\n
LOCATION:FW26
END:VEVENT
END:VCALENDAR