Using Verification Tools for Automatic Parallelisation

Mike Dodds (University of Cambridge)

Info

Date	8th May 2012 (week 3, Trinity Term 2012)
Time	16:30
Place	Lecture Theatre B

Abstract

Constructing correct concurrent programs is tricky. In order to write a program that is free of bugs, the programmer must carefully avoid errors arising from interactions between threads. An appealing alternative is automatic parallelisation -- automatically constructing a concurrent program from a simpler sequential program. The programmer can write a sequential program, ignoring interactions between threads, yet reap much of the benefit of concurrency.

In this talk, I will describe a parallelisation analysis built on verification technology. Verification can extract deep information inaccessible to standard compiler optimisations. Our analysis assumes a sequential program verified using separation logic, and uses the verification information to automatically identify parts of the program that can run in parallel. Unlike previous approaches, our analysis can inject synchronisation constructs to enforce necessary data-dependencies. We generate a proof along with a concurrent program, so the resulting concurrent programs are verified by construction.

Speaker bio

Mike Dodds is a postdoc working at the University of Cambridge. His research focusses on verifying complex concurrent algorithms. Dodds was a co-developer of deny-guarantee, a version of separation logic aimed at modular concurrent reasoning. Dodds is a developer on coreStar, a language-agnostic proof tool for separation logic. He has also worked on using separation logic to inject parallelism into sequential programs. He is currently working on verifying algorithms on relaxed memory systems -- in particular, on the new C11 model.