IMDEA Software

Iniciativa IMDEA

Inicio > Eventos > Charlas Invitadas > 2012 > Recovering Disjointness from Concurrent Sharing
Esta página aún no ha sido traducida. A continuación se muestra la página en inglés.

Mike Dodds

miércoles 23 de mayo de 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.