Automatic analysis of consistency properties of distributed transaction systems in maude

Si Liu, Peter Csaba Ölveczky, Min Zhang, Qi Wang, José 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
EditorsLijun Zhang, Tomáš Vojnar
PublisherSpringer-Verlag Berlin Heidelberg
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

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Automatic analysis of consistency properties of distributed transaction systems in maude'. Together they form a unique fingerprint.

  • 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 L. Zhang, & T. Vojnar (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 Berlin Heidelberg. https://doi.org/10.1007/978-3-030-17465-1_3