Proving Correctness of Highly-Concurrent Linearisable Objects

Abstract : We study a family of implementations for linked lists using fine-grain synchronisation. This approach enables greater concurrency, but correctness is a greater challenge than for classical, coarse-grain synchronisation. Our examples are demonstrative of common design patterns such as lock coupling, optimistic, and lazy synchronisation. Although they are are highly concurrent, we prove that they are linearisable, safe, and they correctly implement a high-level abstraction. Our proofs illustrate the power and applicability of rely-guarantee reasoning, as well of some of its limitations. The examples of the paper establish a benchmark challenge for other reasoning techniques.
Keywords : syn formel
Type de document :
Communication dans un congrès
PPoPP 2006 - 11th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, Mar 2006, New York, United States. ACM, pp.129--136, 2006, 〈10.1145/1122971.1122992〉
Liste complète des métadonnées

Littérature citée [21 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01248204
Contributeur : Alain Monteil <>
Soumis le : jeudi 24 décembre 2015 - 09:43:08
Dernière modification le : vendredi 31 août 2018 - 09:25:54

Fichier

PPoPP-2006-listRG.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Viktor Vafeiadis, Maurice Herlihy, Tony Hoare, Marc Shapiro. Proving Correctness of Highly-Concurrent Linearisable Objects. PPoPP 2006 - 11th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, Mar 2006, New York, United States. ACM, pp.129--136, 2006, 〈10.1145/1122971.1122992〉. 〈hal-01248204〉

Partager

Métriques

Consultations de la notice

139

Téléchargements de fichiers

115