BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Modular Reasoning for Deterministic Parallelism - Mike Dodds\, Uni
 versity of Cambridge
DTSTART:20110121T140000Z
DTEND:20110121T150000Z
UID:TALK29284@talks.cam.ac.uk
CONTACT:Bjarki Holm
DESCRIPTION:Weaving a concurrency control protocol into a program is diffi
 cult and error-prone. One way to alleviate this burden is \\emph{determini
 stic parallelism}. In this well-studied approach to parallelisation\, a se
 quential program is annotated with sections that can execute concurrently\
 , with automatically injected control constructs used to ensure observable
  behaviour consistent with the original program.\n\nThis paper examines th
 e formal specification and verification of these constructs. Our high-leve
 l specification defines the conditions necessary for correct execution\; t
 hese conditions reflect program dependencies necessary to ensure determini
 stic behaviour. We connect the high-level specification used by clients of
  the library with the low-level library implementation\, to prove that a c
 lient's requirements for determinism are enforced. Significantly\, we can 
 reason about program and library correctness without breaking abstraction 
 boundaries.\n\nTo achieve this\, we use concurrent abstract predicates\, b
 ased on separation logic\, to encapsulate racy behaviour in the library's 
 implementation. To allow generic specifications of libraries that can be i
 nstantiated by client programs\, we extend the logic with higher-order par
 ameters and quantification. We show that our high-level specification abst
 racts the details of deterministic parallelism by verifying two different 
 low-level implementations of the library.\n
LOCATION:Room FW11\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR