BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Deny-guarantee reasoning - Mike Dodds (University of Cambridge)
DTSTART:20081103T124500Z
DTEND:20081103T140000Z
UID:TALK14827@talks.cam.ac.uk
CONTACT:Matthew Parkinson
DESCRIPTION:Rely-guarantee is a well-established approach to reasoning abo
 ut\nconcurrent programs that use parallel composition.  However\, parallel
 \ncomposition is not how concurrency is structured in real systems.\nInste
 ad\, threads are started by `fork' and collected with `join'\ncommands.  T
 his style of concurrency cannot be reasoned about using\nrely-guarantee\, 
 as the life-time of a thread can be scoped\ndynamically.  With parallel co
 mposition the scope is static.\n\nIn this talk\, we will describe deny-gua
 rantee reasoning\, a\nreformulation of rely-guarantee that enables reasoni
 ng about\ndynamically scoped concurrency.  Deny-guarantee builds on ideas 
 from\nseparation logic to allow interference to be dynamically split and\n
 recombined\, in a similar way that separation logic splits and joins\nheap
 s. To allow this splitting\, the rely is inverted to give a deny\,\nspecif
 ying what the environment cannot do. We illustrate the use of\nour proof s
 ystem with examples\, and show that it can encode all the\noriginal rely-g
 uarantee proofs.\n\n\nJoint work with Xinyu Feng\, Matthew Parkinson and V
 iktor Vafeiadis.
LOCATION:FW26
END:VEVENT
END:VCALENDAR