RSS

Recovering Disjointness from Concurrent Sharing


http://www.cl.cam.ac.uk/~md466
14/09/2011
Intervenant(s) : Mike Dodds (Université de Cambridge)
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.
---
Mike Dodds est post-doc à l'université de Cambridge. Sa recherche porte sur le raisonnement modulaire autour des programmes concurrents utilisant des pointeurs. Il a à son actif des méthodes de raisonnement et de preuve sur les processeurs multicœur, sur les objets partagés comme les maps ou les index, sur la mémoire faiblement cohérente, et l'utilisation des techniques rely-guarantee et logique de séparation.
Plus d'informations ici
Marc.Shapiro (at) nulllip6.fr
 Mentions légales
Carte du site |