Séminaire des équipes de recherche
Recovering Disjointness from Concurrent Sharing
Free admission at 14h.
- Date : 14/09/2011
- Place : Université Pierre et Marie Curie (UPMC), LIP6 - 4, place Jussieu, Paris 5ème - salle 25-26/105
- Guest(s) : Mike Dodds, Université de Cambridge
- Organiser(s) : REGAL
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, reaping the benefits of disjointness.