BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Higher Order Actions in Deny-Guarantee - Mike Dodds (University of
  Cambridge)
DTSTART:20090629T114500Z
DTEND:20090629T130000Z
UID:TALK18508@talks.cam.ac.uk
CONTACT:Sam Staton
DESCRIPTION: Describing interactions between threads is the key to underst
 anding  \nconcurrent\n  algorithms. In rely-guarantee reasoning\, interact
 ions between\n  threads are modelled abstractly by relations describing\n 
  interference on the shared state. Using relations simplifies\n  reasoning
 \, but makes it difficult to specify temporal properties\n  where interfer
 ence changes over time.\n\n  Deny-guarantee is an extension of rely-guaran
 tee that uses a\n  separation-logic to dynamically partition interference 
 between\n  threads. We have used deny-guarantee to define actions\n  which
  can rewrite interference. Hence\, we consider our actions\n  to be higher
 -order. Our actions can capture temporal properties of  interference\,  an
 d so they allow more state to be thread-local and often avoid\n  the need 
 for auxiliary state. Our approach permits proofs that\n  are more elegant 
 than the equivalent proofs in rely-guarantee.\n\n  Joint work with Matthew
  Parkinson.\n\n
LOCATION:Room FW26\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR