University of Cambridge > Talks.cam > Logic and Semantics Seminar (Computer Laboratory) > Modular Reasoning for Deterministic Parallelism

Modular Reasoning for Deterministic Parallelism

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Bjarki Holm.

Weaving a concurrency control protocol into a program is difficult and error-prone. One way to alleviate this burden is \emph{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.

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2020 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity