ROLA: A new distributed transaction protocol and its formal analysis

Si Liu, Peter Csaba Ölveczky, Keshav Santhanam, Qi Wang, Indranil Gupta, José Meseguer

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

Abstract

Designers of distributed database systems face the choice between stronger consistency guarantees and better performance. A number of applications only require read atomicity (RA) and prevention of lost updates (PLU). Existing distributed database systems that meet these requirements also provide additional stronger consistency guarantees (such as causal consistency), and therefore incur lower performance. In this paper we define a new distributed transaction protocol, ROLA, that targets applications where only RA and PLU are needed. We formally model ROLA in Maude. We then perform model checking to analyze both the correctness and the performance of ROLA. For correctness, we use standard model checking to analyze ROLA’s satisfaction of RA and PLU. To analyze performance we: (a) use statistical model checking to analyze key performance properties; and (b) compare these performance results with those obtained by analyzing in Maude the well-known protocol Walter. Our results show that ROLA outperforms Walter.

Original languageEnglish (US)
Title of host publicationFundamental Approaches to Software Engineering - 21st International Conference, FASE 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Proceedings
EditorsAndy Schurr, Alessandra Russo
PublisherSpringer-Verlag
Pages77-93
Number of pages17
ISBN (Print)9783319893624
DOIs
StatePublished - Jan 1 2018
Event21st International Conference on Fundamental Approaches to Software Engineering, FASE 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018 - Thessaloniki, Greece
Duration: Apr 16 2018Apr 20 2018

Publication series

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

Other

Other21st International Conference on Fundamental Approaches to Software Engineering, FASE 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018
CountryGreece
CityThessaloniki
Period4/16/184/20/18

Fingerprint

Formal Analysis
Model checking
Distributed database systems
Transactions
Network protocols
Atomicity
Distributed Database System
Model Checking
Maude
Strong Consistency
Update
Correctness
Statistical Model
Standard Model
Target
Requirements

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Liu, S., Ölveczky, P. C., Santhanam, K., Wang, Q., Gupta, I., & Meseguer, J. (2018). ROLA: A new distributed transaction protocol and its formal analysis. In A. Schurr, & A. Russo (Eds.), Fundamental Approaches to Software Engineering - 21st International Conference, FASE 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Proceedings (pp. 77-93). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10802 LNCS). Springer-Verlag. https://doi.org/10.1007/978-3-319-89363-1_5

ROLA : A new distributed transaction protocol and its formal analysis. / Liu, Si; Ölveczky, Peter Csaba; Santhanam, Keshav; Wang, Qi; Gupta, Indranil; Meseguer, José.

Fundamental Approaches to Software Engineering - 21st International Conference, FASE 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Proceedings. ed. / Andy Schurr; Alessandra Russo. Springer-Verlag, 2018. p. 77-93 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10802 LNCS).

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

Liu, S, Ölveczky, PC, Santhanam, K, Wang, Q, Gupta, I & Meseguer, J 2018, ROLA: A new distributed transaction protocol and its formal analysis. in A Schurr & A Russo (eds), Fundamental Approaches to Software Engineering - 21st International Conference, FASE 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 10802 LNCS, Springer-Verlag, pp. 77-93, 21st International Conference on Fundamental Approaches to Software Engineering, FASE 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, 4/16/18. https://doi.org/10.1007/978-3-319-89363-1_5
Liu S, Ölveczky PC, Santhanam K, Wang Q, Gupta I, Meseguer J. ROLA: A new distributed transaction protocol and its formal analysis. In Schurr A, Russo A, editors, Fundamental Approaches to Software Engineering - 21st International Conference, FASE 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Proceedings. Springer-Verlag. 2018. p. 77-93. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-319-89363-1_5
Liu, Si ; Ölveczky, Peter Csaba ; Santhanam, Keshav ; Wang, Qi ; Gupta, Indranil ; Meseguer, José. / ROLA : A new distributed transaction protocol and its formal analysis. Fundamental Approaches to Software Engineering - 21st International Conference, FASE 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Proceedings. editor / Andy Schurr ; Alessandra Russo. Springer-Verlag, 2018. pp. 77-93 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{a99362fac99a4496be6d614728cb14c5,
title = "ROLA: A new distributed transaction protocol and its formal analysis",
abstract = "Designers of distributed database systems face the choice between stronger consistency guarantees and better performance. A number of applications only require read atomicity (RA) and prevention of lost updates (PLU). Existing distributed database systems that meet these requirements also provide additional stronger consistency guarantees (such as causal consistency), and therefore incur lower performance. In this paper we define a new distributed transaction protocol, ROLA, that targets applications where only RA and PLU are needed. We formally model ROLA in Maude. We then perform model checking to analyze both the correctness and the performance of ROLA. For correctness, we use standard model checking to analyze ROLA’s satisfaction of RA and PLU. To analyze performance we: (a) use statistical model checking to analyze key performance properties; and (b) compare these performance results with those obtained by analyzing in Maude the well-known protocol Walter. Our results show that ROLA outperforms Walter.",
author = "Si Liu and {\"O}lveczky, {Peter Csaba} and Keshav Santhanam and Qi Wang and Indranil Gupta and Jos{\'e} Meseguer",
year = "2018",
month = "1",
day = "1",
doi = "10.1007/978-3-319-89363-1_5",
language = "English (US)",
isbn = "9783319893624",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer-Verlag",
pages = "77--93",
editor = "Andy Schurr and Alessandra Russo",
booktitle = "Fundamental Approaches to Software Engineering - 21st International Conference, FASE 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Proceedings",

}

TY - GEN

T1 - ROLA

T2 - A new distributed transaction protocol and its formal analysis

AU - Liu, Si

AU - Ölveczky, Peter Csaba

AU - Santhanam, Keshav

AU - Wang, Qi

AU - Gupta, Indranil

AU - Meseguer, José

PY - 2018/1/1

Y1 - 2018/1/1

N2 - Designers of distributed database systems face the choice between stronger consistency guarantees and better performance. A number of applications only require read atomicity (RA) and prevention of lost updates (PLU). Existing distributed database systems that meet these requirements also provide additional stronger consistency guarantees (such as causal consistency), and therefore incur lower performance. In this paper we define a new distributed transaction protocol, ROLA, that targets applications where only RA and PLU are needed. We formally model ROLA in Maude. We then perform model checking to analyze both the correctness and the performance of ROLA. For correctness, we use standard model checking to analyze ROLA’s satisfaction of RA and PLU. To analyze performance we: (a) use statistical model checking to analyze key performance properties; and (b) compare these performance results with those obtained by analyzing in Maude the well-known protocol Walter. Our results show that ROLA outperforms Walter.

AB - Designers of distributed database systems face the choice between stronger consistency guarantees and better performance. A number of applications only require read atomicity (RA) and prevention of lost updates (PLU). Existing distributed database systems that meet these requirements also provide additional stronger consistency guarantees (such as causal consistency), and therefore incur lower performance. In this paper we define a new distributed transaction protocol, ROLA, that targets applications where only RA and PLU are needed. We formally model ROLA in Maude. We then perform model checking to analyze both the correctness and the performance of ROLA. For correctness, we use standard model checking to analyze ROLA’s satisfaction of RA and PLU. To analyze performance we: (a) use statistical model checking to analyze key performance properties; and (b) compare these performance results with those obtained by analyzing in Maude the well-known protocol Walter. Our results show that ROLA outperforms Walter.

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

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

U2 - 10.1007/978-3-319-89363-1_5

DO - 10.1007/978-3-319-89363-1_5

M3 - Conference contribution

AN - SCOPUS:85045659219

SN - 9783319893624

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

SP - 77

EP - 93

BT - Fundamental Approaches to Software Engineering - 21st International Conference, FASE 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Proceedings

A2 - Schurr, Andy

A2 - Russo, Alessandra

PB - Springer-Verlag

ER -