Vous pouvez vous abonner à nos annonces de séminaires http://gallium.inria.fr/seminaires/ S E M I N A I R E __ / _` _ / / o /| /| __ __ __ __ _ _ / ) __) / / / / / /\/| ----- / |/ | / )(_ / / ) ) ) __) (___/ (_/ (_ (_ / (__/ / | / | (__/ __)(_ (__/ (_/ (_/ I N R I A - Rocquencourt Amphi Turing du bâtiment 1 VENDREDI 16 septembre, 10h30 ---------- Mike Dodds ---------- Cambridge University =============================================== Recovering Disjointness from Concurrent Sharing =============================================== 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.