A Formal Analysis of the Global Sequence Protocol

Abstract : The Global Sequence Protocol (GSP) is an operational model for replicated data stores, in which updates propagate asynchronously. We introduce the GSP-calculus as a formal model for GSP. We give a formal account for its proposed implementation, which addresses communication failures and compact representation of data, and use simulation to prove that the implementation is correct. Then, we use the GSP-calculus to reason about execution histories and prove ordering guarantees, such as read my writes, monotonic reads, causality and consistent prefix. We also prove that GSP extended with synchronous updates provides strong consistency guarantees.
Type de document :
Communication dans un congrès
Alberto Lluch Lafuente; José Proença. 18th International Conference on Coordination Languages and Models (COORDINATION), Jun 2016, Heraklion, Greece. Springer International Publishing, Lecture Notes in Computer Science, LNCS-9686, pp.175-191, 2016, Coordination Models and Languages. 〈10.1007/978-3-319-39519-7_11〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01631716
Contributeur : Hal Ifip <>
Soumis le : jeudi 9 novembre 2017 - 16:13:48
Dernière modification le : mercredi 1 août 2018 - 15:02:03
Document(s) archivé(s) le : samedi 10 février 2018 - 14:28:00

Fichier

 Accès restreint
Fichier visible le : 2019-01-01

Connectez-vous pour demander l'accès au fichier

Licence


Distributed under a Creative Commons Paternité 4.0 International License

Identifiants

Citation

Hernán Melgratti, Christian Roldán. A Formal Analysis of the Global Sequence Protocol. Alberto Lluch Lafuente; José Proença. 18th International Conference on Coordination Languages and Models (COORDINATION), Jun 2016, Heraklion, Greece. Springer International Publishing, Lecture Notes in Computer Science, LNCS-9686, pp.175-191, 2016, Coordination Models and Languages. 〈10.1007/978-3-319-39519-7_11〉. 〈hal-01631716〉

Partager

Métriques

Consultations de la notice

28