BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:The Importance of Being Linearizable - Alexey Gotsman\, IMDEA Soft
 ware Institute
DTSTART:20111107T124500Z
DTEND:20111107T140000Z
UID:TALK33287@talks.cam.ac.uk
CONTACT:Peter Sewell
DESCRIPTION:Specifications of concurrent libraries are commonly given by t
 he well-known notion of linearizability. However\, to date linearizability
  has been no more than a box to be ticked in a paper with a new concurrent
  algorithm\, lest it should get rejected. The notion has not even been def
 ined for realistic settings in which concurrent algorithms usually get use
 d! Recently\, we have been trying to show that linearizability is more imp
 ortant than that by generalising it to realistic settings and establishing
  theorems that allow exploiting it to verify concurrent programs compositi
 onally. \n\nIn this talk\, I will present our definition of linearizabilit
 y on the TSO weak memory model (used by Intel processors) and a theorem sh
 owing that\, while verifying a client using a concurrent library\, we can 
 soundly replace the library by another one related to the original library
  by our generalisation of linearizability. \n\nThis is joint work with Seb
 astian Burckhardt\, Madan Musuvathi (Microsoft Research) and Hongseok Yang
  (University of Oxford\, UK).\n
LOCATION:FW26
END:VEVENT
END:VCALENDAR