[Pl-seminar] 2/7: Mike Dodds, "Recovering Disjointness from Concurrent Sharing"

[Aaron Turon]

NEU Programming Languages Seminar presents

Mike Dodds
Cambridge University

Tuesday 2/7
11:45AM
Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

Recovering Disjointness from Concurrent Sharing

Disjointness between resources is an extraordinarily useful property
when verifying concurrent programs. Threads that access mutually
disjoint resources can be reasoned about locally, ignoring
interleavings; this is the core insight behind Concurrent Separation
Logic. However, concurrent modules often share resources internally,
frustrating disjoint reasoning. In this talk, I will suggest that
sharing is often irrelevant to the clients of these modules, and can
be hidden. I will show how separation logic can be used to hide
irrelevant sharing and recover disjoint reasoning. I will motivate
this with the example of a concurrent index, and show how some
high-level sharing between threads can be maintained, reaping the
benefits of disjointness.

--

Mike Dodds is a postdoc working at the University of Cambridge. His
research is focussed is 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. His current work focusses on verifying algorithms
on relaxed memory architectures -- in particular, on the C++11 model.