Wednesday, May 23, 2012
10:45am IMDEA conference room
Mike Dodds, Post-doctoral Researcher, University of Cambridge, United Kingdom
Recovering Disjointness from Concurrent Sharing
Abstract:
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.