IMDEA Software

IMDEA initiative

Home > Events > Invited Talks > 2012 > Recovering Disjointness from Concurrent Sharing

Mike Dodds

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.