TY - GEN
T1 - Formalizing and Checking Multilevel Consistency
AU - Bouajjani, Ahmed
AU - Enea, Constantin
AU - Mukund, Madhavan
AU - Shenoy R, Gautham
AU - Suresh, S. P.
N1 - Publisher Copyright:
© 2020, Springer Nature Switzerland AG.
PY - 2020/1/1
Y1 - 2020/1/1
N2 - Developers of distributed data-stores must trade consistency for performance and availability. Such systems may in fact implement weak consistency models, e.g., causal consistency or eventual consistency, corresponding to different costs and guarantees to the clients. We consider the case of distributed systems that offer not just one level of consistency but multiple levels of consistency to the clients. This corresponds to many practical situations. For instance, popular data-stores such as Amazon DynamoDB and Apache’s Cassandra allow applications to tag each query within the same session with a separate consistency level. In this paper, we provide a formal framework for the specification of multilevel consistency, and we address the problem of checking the conformance of a computation to such a specification. We provide a principled algorithmic approach to this problem and apply it to several instances of models with multilevel consistency.
AB - Developers of distributed data-stores must trade consistency for performance and availability. Such systems may in fact implement weak consistency models, e.g., causal consistency or eventual consistency, corresponding to different costs and guarantees to the clients. We consider the case of distributed systems that offer not just one level of consistency but multiple levels of consistency to the clients. This corresponds to many practical situations. For instance, popular data-stores such as Amazon DynamoDB and Apache’s Cassandra allow applications to tag each query within the same session with a separate consistency level. In this paper, we provide a formal framework for the specification of multilevel consistency, and we address the problem of checking the conformance of a computation to such a specification. We provide a principled algorithmic approach to this problem and apply it to several instances of models with multilevel consistency.
U2 - 10.1007/978-3-030-39322-9_18
DO - 10.1007/978-3-030-39322-9_18
M3 - Conference contribution
AN - SCOPUS:85079096514
SN - 9783030393212
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 379
EP - 400
BT - Verification, Model Checking, and Abstract Interpretation - 21st International Conference, VMCAI 2020, Proceedings
A2 - Beyer, Dirk
A2 - Zufferey, Damien
PB - Springer
T2 - 21st International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2020
Y2 - 16 January 2020 through 21 January 2020
ER -