BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Proving Liveness Properties of Non-blocking Data Structures - Alex
 ey Gotsman (ARG)
DTSTART:20080603T120000Z
DTEND:20080603T130000Z
UID:TALK11660@talks.cam.ac.uk
CONTACT:Thomas Tuerk
DESCRIPTION:In non-blocking concurrency\, instead of using mutual exclusio
 n to guard access to shared data structures\, threads attempt to make conc
 urrent changes\, looping and trying again if a particular attempt fails to
  achieve\nthe desired result. Algorithms operating on non-blocking data st
 ructures are complicated and hard to get right\, hence\, their formal veri
 fication is highly desirable. The work in this direction has so far focuse
 d on verifying\nsafety properties of these algorithms\, such as memory saf
 ety or linearizability. However\, operations on non-blocking data structur
 es also have to satisfy certain liveness properties (wait-freedom\, lock-f
 reedom\, and\nobstruction-freedom) that ensure their termination under var
 ious conditions. In this talk I will present a compositional proof system 
 for verifying these properties based on a combination of rely-guarantee re
 asoning and separation logic.\n\nThis is joint work with Byron Cook\, Matt
 hew Parkinson\, and Viktor Vafeiadis.\n
LOCATION:Computer Laboratory\, William Gates Building\, Room SS03
END:VEVENT
END:VCALENDAR