Recovering Disjointness from Concurrent Sharing

May 23, 2012

Mike Dodds


Recovering Disjointness from Concurrent Sharing

Time:   10:45am
Location:   IMDEA conference room

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.