Replicated Data Types: Specification, Verification, Optimality

Abstract : Geographically distributed systems often rely on replicated eventu- ally consistent data stores to achieve availability and performance. To resolve conflicting updates at different replicas, researchers and practitioners have proposed specialized consistency protocols, called replicated data types, that implement objects such as reg- isters, counters, sets or lists. Reasoning about replicated data types has however not been on par with comparable work on abstract data types and concurrent data types, lacking specifications, correctness proofs, and optimality results. To fill in this gap, we propose a framework for specifying repli- cated data types using relations over events and verifying their im- plementations using replication-aware simulations. We apply it to 7 existing implementations of 4 data types with nontrivial conflict- resolution strategies and optimizations (last-writer-wins register, counter, multi-value register and observed-remove set). We also present a novel technique for obtaining lower bounds on the worst- case space overhead of data type implementations and use it to prove optimality of 4 implementations. Finally, we show how to specify consistency of replicated stores with multiple objects ax- iomatically, in analogy to prior work on weak memory models. Overall, our work provides foundational reasoning tools to support research on replicated eventually consistent stores
Type de document :
Communication dans un congrès
POPL 2014: 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Jan 2014, San Diego, CA, United States. ACM, pp.271-284, 2014, 〈10.1145/2535838.2535848〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-00934311
Contributeur : Marc Shapiro <>
Soumis le : mardi 21 janvier 2014 - 18:10:29
Dernière modification le : jeudi 11 janvier 2018 - 06:20:06
Document(s) archivé(s) le : mardi 22 avril 2014 - 10:02:53

Fichier

Replicated_Data_Types-_Specifi...
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Sebastian Burckhardt, Alexey Gotsman, Hongseok Yang, Marek Zawirski. Replicated Data Types: Specification, Verification, Optimality. POPL 2014: 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Jan 2014, San Diego, CA, United States. ACM, pp.271-284, 2014, 〈10.1145/2535838.2535848〉. 〈hal-00934311〉

Partager

Métriques

Consultations de la notice

912

Téléchargements de fichiers

697