Formalizing and Checking Multilevel Consistency

Ahmed Bouajjani; Constantin Enea; Madhavan Mukund; Gautham Shenoy R; S. P. Suresh

doi:10.1007/978-3-030-39322-9_18

Formalizing and Checking Multilevel Consistency

Ahmed Bouajjani
, Constantin Enea
, Madhavan Mukund
, Gautham Shenoy R
, S. P. Suresh

Laboratoire de Probabilités et Modèles Aléatoires
Chennai Mathematical Institute
CNRS UMI 2000 ReLaX

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

3 Citations (Scopus)

Abstract

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.

Original language	English
Title of host publication	Verification, Model Checking, and Abstract Interpretation - 21st International Conference, VMCAI 2020, Proceedings
Editors	Dirk Beyer, Damien Zufferey
Publisher	Springer
Pages	379-400
Number of pages	22
ISBN (Print)	9783030393212
DOIs	https://doi.org/10.1007/978-3-030-39322-9_18
Publication status	Published - 1 Jan 2020
Externally published	Yes
Event	21st International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2020 - New Orleans, United States Duration: 16 Jan 2020 → 21 Jan 2020

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	11990 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	21st International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2020
Country/Territory	United States
City	New Orleans
Period	16/01/20 → 21/01/20

Access to Document

10.1007/978-3-030-39322-9_18

Cite this

Bouajjani, A., Enea, C., Mukund, M., Shenoy R, G., & Suresh, S. P. (2020). Formalizing and Checking Multilevel Consistency. In D. Beyer, & D. Zufferey (Eds.), Verification, Model Checking, and Abstract Interpretation - 21st International Conference, VMCAI 2020, Proceedings (pp. 379-400). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11990 LNCS). Springer. https://doi.org/10.1007/978-3-030-39322-9_18

Bouajjani, Ahmed ; Enea, Constantin ; Mukund, Madhavan et al. / Formalizing and Checking Multilevel Consistency. Verification, Model Checking, and Abstract Interpretation - 21st International Conference, VMCAI 2020, Proceedings. editor / Dirk Beyer ; Damien Zufferey. Springer, 2020. pp. 379-400 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{befd390cbcb244a88a4b9a950b030122,

title = "Formalizing and Checking Multilevel Consistency",

abstract = "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{\textquoteright}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.",

author = "Ahmed Bouajjani and Constantin Enea and Madhavan Mukund and \{Shenoy R\}, Gautham and Suresh, \{S. P.\}",

note = "Publisher Copyright: {\textcopyright} 2020, Springer Nature Switzerland AG.; 21st International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2020 ; Conference date: 16-01-2020 Through 21-01-2020",

year = "2020",

month = jan,

day = "1",

doi = "10.1007/978-3-030-39322-9\_18",

language = "English",

isbn = "9783030393212",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "379--400",

editor = "Dirk Beyer and Damien Zufferey",

booktitle = "Verification, Model Checking, and Abstract Interpretation - 21st International Conference, VMCAI 2020, Proceedings",

}

Bouajjani, A, Enea, C, Mukund, M, Shenoy R, G & Suresh, SP 2020, Formalizing and Checking Multilevel Consistency. in D Beyer & D Zufferey (eds), Verification, Model Checking, and Abstract Interpretation - 21st International Conference, VMCAI 2020, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 11990 LNCS, Springer, pp. 379-400, 21st International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2020, New Orleans, United States, 16/01/20. https://doi.org/10.1007/978-3-030-39322-9_18

Formalizing and Checking Multilevel Consistency. / Bouajjani, Ahmed; Enea, Constantin; Mukund, Madhavan et al.
Verification, Model Checking, and Abstract Interpretation - 21st International Conference, VMCAI 2020, Proceedings. ed. / Dirk Beyer; Damien Zufferey. Springer, 2020. p. 379-400 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11990 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

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.

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 -

Bouajjani A, Enea C, Mukund M, Shenoy R G, Suresh SP. Formalizing and Checking Multilevel Consistency. In Beyer D, Zufferey D, editors, Verification, Model Checking, and Abstract Interpretation - 21st International Conference, VMCAI 2020, Proceedings. Springer. 2020. p. 379-400. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-030-39322-9_18

Formalizing and Checking Multilevel Consistency

Abstract

Publication series

Conference

Access to Document

Fingerprint

Cite this