'Cause I'm strong enough: Reasoning about consistency choices in distributed systems

Alexey Gotsman, Hongseok Yang, Carla Ferreira, Mahsa Najafzadeh, Marc Shapiro

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

55 Citations (Scopus)

Abstract

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.

Original languageEnglish
Title of host publicationPOPL 2016 - Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
PublisherAssociation for Computing Machinery
Pages371-384
Number of pages14
Volume20-22-January-2016
ISBN (Electronic)9781450335492
DOIs
Publication statusPublished - 8 Apr 2016
Event43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016 - St. Petersburg, United States
Duration: 20 Jan 201622 Jan 2016

Conference

Conference43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016
CountryUnited States
CitySt. Petersburg
Period20/01/1622/01/16

Keywords

  • Causal consistency
  • Integrity invariants
  • Replication

Fingerprint

Dive into the research topics of ''Cause I'm strong enough: Reasoning about consistency choices in distributed systems'. Together they form a unique fingerprint.

Cite this