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:20090310T130000Z
DTEND:20090310T140000Z
UID:TALK17373@talks.cam.ac.uk
CONTACT:Sam Staton
DESCRIPTION:Rely-guarantee is a well-established approach to reasoning abo
 ut concurrent programs that use parallel composition. However\, parallel c
 omposition is not how concurrency is structured in real systems. Instead\,
  threads are started by `fork' and collected with `join' commands. This st
 yle of concurrency cannot be reasoned about using rely-guarantee\, as the 
 life-time of a thread can be scoped dynamically. With parallel composition
  the scope is static.\n\nIn this paper\, we introduce deny-guarantee reaso
 ning\, a reformulation of rely-guarantee that enables reasoning about dyna
 mically scoped concurrency. We build on ideas from separation logic to all
 ow interference to be dynamically split and recombined\, in a similar way 
 that separation logic splits and joins heaps. To allow this splitting\, we
  use deny and guarantee permissions: a deny permission specifies that the 
 environment cannot do an action\, and guarantee permission allow us to do 
 an action. We illustrate the use of our proof system with examples\, and s
 how that it can encode all the original rely-guarantee proofs. We also pre
 sent the semantics and soundness of the deny-guarantee method.\n\nJoint wo
 rk by Mike Dodds\, Xinyu Feng\, Matthew Parkinson\, Viktor Vafeiadis.
LOCATION:Room SS03\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR