'Cause I'm Strong Enough: Reasoning about Consistency Choices in Distributed Systems - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2016

'Cause I'm Strong Enough: Reasoning about Consistency Choices in Distributed Systems

Résumé

Large-scale distributed systems often rely on replicated databases that allow a programmer to request different data consistency guarantees for different operations, and thereby control their performance. Using such databases is far from trivial: requesting stronger consistency in too many places may hurt performance, and requesting it in too few places may violate correctness. To help programmers in this task, we propose the first proof rule for establishing that a particular choice of consistency guarantees for various operations on a replicated database is enough to ensure the preservation of a given data integrity invariant. Our rule is modular: it allows reasoning about the behaviour of every operation separately under some assumption on the behaviour of other operations. This leads to simple reasoning, which we have automated in an SMT-based tool. We present a nontrivial proof of soundness of our rule and illustrate its use on several examples.

Domaines

Autre [cs.OH]
Fichier principal
Vignette du fichier
CISE-POPL-2016.pdf (764.95 Ko) Télécharger le fichier
cex1.pdf (26.96 Ko) Télécharger le fichier
cex2.pdf (27.49 Ko) Télécharger le fichier
exec.pdf (26.09 Ko) Télécharger le fichier
exec2.pdf (24.75 Ko) Télécharger le fichier
exec3.pdf (28.59 Ko) Télécharger le fichier
exec4.pdf (18.86 Ko) Télécharger le fichier
logic.pdf (781.19 Ko) Télécharger le fichier
messages3.pdf (31.2 Ko) Télécharger le fichier
messages4.pdf (24.84 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Origine : Fichiers produits par l'(les) auteur(s)
Origine : Fichiers produits par l'(les) auteur(s)
Origine : Fichiers produits par l'(les) auteur(s)
Origine : Fichiers produits par l'(les) auteur(s)
Origine : Fichiers produits par l'(les) auteur(s)
Origine : Fichiers produits par l'(les) auteur(s)
Origine : Fichiers produits par l'(les) auteur(s)
Origine : Fichiers produits par l'(les) auteur(s)
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-01243192 , version 1 (14-12-2015)

Identifiants

Citer

Alexey Gotsman, Hongseok Yang, Carla Ferreira, Mahsa Najafzadeh, Marc Shapiro. 'Cause I'm Strong Enough: Reasoning about Consistency Choices in Distributed Systems. Symposium on Principles of Programming Languages, Jan 2016, Saint Petersburg, FL, United States. pp.371-384, ⟨10.1145/2837614.2837625⟩. ⟨hal-01243192⟩
346 Consultations
1325 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More