Inria
Inria.fr
Inria Channel
Séminaires des équipes de recherche
Recovering Disjointness from Concurrent Sharing
Inria - Rocquencourt, amphithéâtre Alan Turing, bâtiment 1.
Entrée libre à 10 h 30
- Date : 16/09/2011
- Place : Inria - Rocquencourt, amphithéâtre Alan Turing, bâtiment 1.
- Guests : Mike Dodds - Cambridge University
- Organisers : Gallium - Moscova
Disjointness is an extraordinarily useful property when reasoning about 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 should 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 can be maintained, while still reaping the benefits of disjointness.
Keywords: Paris - Rocquencourt Séminaire Moscova Gallium
