Modular reasoning for deterministic parallelism

Mike Dodds, Suresh Jagannathan, Matthew J. Parkinson

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Weaving a concurrency control protocol into a program is difficult and error-prone. One way to alleviate this burden is deterministic parallelism. In this well-studied approach to parallelisation, a sequential program is annotated with sections that can execute concurrently, with automatically injected control constructs used to ensure observable behaviour consistent with the original program.
This paper examines the formal specification and verification of these constructs. Our high-level specification defines the conditions necessary for correct execution; these conditions reflect program dependencies necessary to ensure deterministic behaviour. We connect the high-level specification used by clients of the library with the low-level library implementation, to prove that a client's requirements for determinism are enforced. Significantly, we can reason about program and library correctness without breaking abstraction boundaries.
To achieve this, we use concurrent abstract predicates, based on separation logic, to encapsulate racy behaviour in the library's implementation. To allow generic specifications of libraries that can be instantiated by client programs, we extend the logic with higher-order parameters and quantification. We show that our high-level specification abstracts the details of deterministic parallelism by verifying two different low-level implementations of the library.
Original languageEnglish
Title of host publicationPOPL '11 Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages
PublisherACM
Pages259-270
Number of pages12
ISBN (Print)978-1-4503-0490-0
DOIs
Publication statusPublished - 26 Jan 2011
Event38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL 2011) - Austin, United States
Duration: 26 Jan 201128 Jan 2011

Conference

Conference38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL 2011)
Country/TerritoryUnited States
CityAustin
Period26/01/1128/01/11

Cite this