Sites Inria

Version française

Séminaires des équipes de recherche

Recovering Disjointness from Concurrent Sharing

Séminaire Gallium - Moscova

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.
  • Guest(s) : Mike Dodds - Cambridge University
  • Organiser(s) : 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