Automatic analysis of consistency properties of distributed transaction systems in maude

Si Liu, Peter Csaba Ölveczky, Min Zhang, Qi Wang, Jose Meseguer

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Many transaction systems distribute, partition, and replicate their data for scalability, availability, and fault tolerance. However, observing and maintaining strong consistency of distributed and partially replicated data leads to high transaction latencies. Since different applications require different consistency guarantees, there is a plethora of consistency properties—from weak ones such as read atomicity through various forms of snapshot isolation to stronger serializability properties—and distributed transaction systems (DTSs) guaranteeing such properties. This paper presents a general framework for formally specifying a DTS in Maude, and formalizes in Maude nine common consistency properties for DTSs so defined. Furthermore, we provide a fully automated method for analyzing whether the DTS satisfies the desired property for all initial states up to given bounds on system parameters. This is based on automatically recording relevant history during a Maude run and defining the consistency properties on such histories. To the best of our knowledge, this is the first time that model checking of all these properties in a unified, systematic manner is investigated. We have implemented a tool that automates our method, and use it to model check state-of-the-art DTSs such as P-Store, RAMP, Walter, Jessy, and ROLA.

Original languageEnglish (US)
Title of host publicationTools and Algorithms for the Construction and Analysis of Systems - 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings
EditorsTomáš Vojnar, Lijun Zhang
PublisherSpringer-Verlag
Pages40-57
Number of pages18
ISBN (Print)9783030174644
DOIs
StatePublished - Jan 1 2019
Event25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems conference series, TACAS 2019 held as part of the 22nd European Joint Conferences on Theory and Practice of Software, ETAPS 2019 - Prague, Czech Republic
Duration: Apr 6 2019Apr 11 2019

Publication series

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

Conference

Conference25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems conference series, TACAS 2019 held as part of the 22nd European Joint Conferences on Theory and Practice of Software, ETAPS 2019
CountryCzech Republic
CityPrague
Period4/6/194/11/19

Fingerprint

Maude
Model checking
Fault tolerance
Transactions
Scalability
Availability
Weak Consistency
Atomicity
Strong Consistency
Snapshot
Fault Tolerance
Model Checking
Isolation
Latency
Partition

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Liu, S., Ölveczky, P. C., Zhang, M., Wang, Q., & Meseguer, J. (2019). Automatic analysis of consistency properties of distributed transaction systems in maude. In T. Vojnar, & L. Zhang (Eds.), Tools and Algorithms for the Construction and Analysis of Systems - 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings (pp. 40-57). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11428 LNCS). Springer-Verlag. https://doi.org/10.1007/978-3-030-17465-1_3

Automatic analysis of consistency properties of distributed transaction systems in maude. / Liu, Si; Ölveczky, Peter Csaba; Zhang, Min; Wang, Qi; Meseguer, Jose.

Tools and Algorithms for the Construction and Analysis of Systems - 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings. ed. / Tomáš Vojnar; Lijun Zhang. Springer-Verlag, 2019. p. 40-57 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11428 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Liu, S, Ölveczky, PC, Zhang, M, Wang, Q & Meseguer, J 2019, Automatic analysis of consistency properties of distributed transaction systems in maude. in T Vojnar & L Zhang (eds), Tools and Algorithms for the Construction and Analysis of Systems - 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 11428 LNCS, Springer-Verlag, pp. 40-57, 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems conference series, TACAS 2019 held as part of the 22nd European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, 4/6/19. https://doi.org/10.1007/978-3-030-17465-1_3
Liu S, Ölveczky PC, Zhang M, Wang Q, Meseguer J. Automatic analysis of consistency properties of distributed transaction systems in maude. In Vojnar T, Zhang L, editors, Tools and Algorithms for the Construction and Analysis of Systems - 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings. Springer-Verlag. 2019. p. 40-57. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-030-17465-1_3
Liu, Si ; Ölveczky, Peter Csaba ; Zhang, Min ; Wang, Qi ; Meseguer, Jose. / Automatic analysis of consistency properties of distributed transaction systems in maude. Tools and Algorithms for the Construction and Analysis of Systems - 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings. editor / Tomáš Vojnar ; Lijun Zhang. Springer-Verlag, 2019. pp. 40-57 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{4557edbfbb90458eb4e957b88704b75d,
title = "Automatic analysis of consistency properties of distributed transaction systems in maude",
abstract = "Many transaction systems distribute, partition, and replicate their data for scalability, availability, and fault tolerance. However, observing and maintaining strong consistency of distributed and partially replicated data leads to high transaction latencies. Since different applications require different consistency guarantees, there is a plethora of consistency properties—from weak ones such as read atomicity through various forms of snapshot isolation to stronger serializability properties—and distributed transaction systems (DTSs) guaranteeing such properties. This paper presents a general framework for formally specifying a DTS in Maude, and formalizes in Maude nine common consistency properties for DTSs so defined. Furthermore, we provide a fully automated method for analyzing whether the DTS satisfies the desired property for all initial states up to given bounds on system parameters. This is based on automatically recording relevant history during a Maude run and defining the consistency properties on such histories. To the best of our knowledge, this is the first time that model checking of all these properties in a unified, systematic manner is investigated. We have implemented a tool that automates our method, and use it to model check state-of-the-art DTSs such as P-Store, RAMP, Walter, Jessy, and ROLA.",
author = "Si Liu and {\"O}lveczky, {Peter Csaba} and Min Zhang and Qi Wang and Jose Meseguer",
year = "2019",
month = "1",
day = "1",
doi = "10.1007/978-3-030-17465-1_3",
language = "English (US)",
isbn = "9783030174644",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer-Verlag",
pages = "40--57",
editor = "Tom{\'a}š Vojnar and Lijun Zhang",
booktitle = "Tools and Algorithms for the Construction and Analysis of Systems - 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings",

}

TY - GEN

T1 - Automatic analysis of consistency properties of distributed transaction systems in maude

AU - Liu, Si

AU - Ölveczky, Peter Csaba

AU - Zhang, Min

AU - Wang, Qi

AU - Meseguer, Jose

PY - 2019/1/1

Y1 - 2019/1/1

N2 - Many transaction systems distribute, partition, and replicate their data for scalability, availability, and fault tolerance. However, observing and maintaining strong consistency of distributed and partially replicated data leads to high transaction latencies. Since different applications require different consistency guarantees, there is a plethora of consistency properties—from weak ones such as read atomicity through various forms of snapshot isolation to stronger serializability properties—and distributed transaction systems (DTSs) guaranteeing such properties. This paper presents a general framework for formally specifying a DTS in Maude, and formalizes in Maude nine common consistency properties for DTSs so defined. Furthermore, we provide a fully automated method for analyzing whether the DTS satisfies the desired property for all initial states up to given bounds on system parameters. This is based on automatically recording relevant history during a Maude run and defining the consistency properties on such histories. To the best of our knowledge, this is the first time that model checking of all these properties in a unified, systematic manner is investigated. We have implemented a tool that automates our method, and use it to model check state-of-the-art DTSs such as P-Store, RAMP, Walter, Jessy, and ROLA.

AB - Many transaction systems distribute, partition, and replicate their data for scalability, availability, and fault tolerance. However, observing and maintaining strong consistency of distributed and partially replicated data leads to high transaction latencies. Since different applications require different consistency guarantees, there is a plethora of consistency properties—from weak ones such as read atomicity through various forms of snapshot isolation to stronger serializability properties—and distributed transaction systems (DTSs) guaranteeing such properties. This paper presents a general framework for formally specifying a DTS in Maude, and formalizes in Maude nine common consistency properties for DTSs so defined. Furthermore, we provide a fully automated method for analyzing whether the DTS satisfies the desired property for all initial states up to given bounds on system parameters. This is based on automatically recording relevant history during a Maude run and defining the consistency properties on such histories. To the best of our knowledge, this is the first time that model checking of all these properties in a unified, systematic manner is investigated. We have implemented a tool that automates our method, and use it to model check state-of-the-art DTSs such as P-Store, RAMP, Walter, Jessy, and ROLA.

UR - http://www.scopus.com/inward/record.url?scp=85064540496&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85064540496&partnerID=8YFLogxK

U2 - 10.1007/978-3-030-17465-1_3

DO - 10.1007/978-3-030-17465-1_3

M3 - Conference contribution

SN - 9783030174644

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 40

EP - 57

BT - Tools and Algorithms for the Construction and Analysis of Systems - 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings

A2 - Vojnar, Tomáš

A2 - Zhang, Lijun

PB - Springer-Verlag

ER -