BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Fine-grained concurrency with separation logic - Uday Reddy\, Univ
 ersity of Birmingham
DTSTART:20061201T140000Z
DTEND:20061201T150000Z
UID:TALK6005@talks.cam.ac.uk
CONTACT:Tom Ridge
DESCRIPTION:Separation Logic is a recent development in programming logic 
 which\nhas been applied by Peter O'Hearn to concurrency based on critical\
 nsections as well as semaphores.  In this work\, we go one step further\na
 nd apply it to fine-grained concurrency.  We note that O'Hearn's\nformulat
 ion of Concurrent Separation Logic is by and large applicable\nto fine-gra
 ined concurrent programs with only minor adaptations.\nHowever\, proving s
 ubstantial properties of such programs involves the\nemployment of sophist
 icated ``permissions'' frameworks so that\ndifferent processes can have di
 fferent levels of access and exchange\nsuch access.\n\nWe illustrate these
  techniques by showing the correctness proof of a\nconcurrent garbage coll
 ector originally studied by Dijkstra et al.\nThe original proof is based o
 n informal reasoning\, and it is said to\nhave been very challenging to en
 sure its validity.  Our techniques\nformalise this proof\, but we find tha
 t there are significant details\nthat need to be filled in.\n\n
LOCATION:FW11
END:VEVENT
END:VCALENDAR