Conference item
'Cause I'm Strong Enough: Reasoning about consistency choices in distributed systems
- 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.
- Publication status:
- Published
- Peer review status:
- Peer reviewed
Actions
Access Document
- Files:
-
-
(Preview, Accepted manuscript, pdf, 773.0KB, Terms of use)
-
- Publisher copy:
- 10.1145/2837614.2837625
Authors
- Publisher:
- Association for Computing Machinery
- Host title:
- 43rd ACM Symposium on Principles of Programming Languages (POPL 2016)
- Journal:
- 43rd ACM Symposium on Principles of Programming Languages (POPL 2016) More from this journal
- Publication date:
- 2016-01-11
- Acceptance date:
- 2015-10-05
- DOI:
- Keywords:
- Pubs id:
-
pubs:581034
- UUID:
-
uuid:cc2026e8-1d0e-4376-87ac-94b240546ef3
- Local pid:
-
pubs:581034
- Source identifiers:
-
581034
- Deposit date:
-
2016-01-03
Terms of use
- Copyright holder:
- Association for Computing Machinery
- Copyright date:
- 2016
- Notes:
- Copyright © 2016 by the Association for Computing Machinery, Inc (ACM). Permission to make digital or hard copies of portions of this work for personal or classroom use is granted without fee provided that the copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted.
If you are the owner of this record, you can report an update to it here: Report update to this record