TY - GEN
T1 - ROLA
T2 - 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
AU - Liu, Si
AU - Ölveczky, Peter Csaba
AU - Santhanam, Keshav
AU - Wang, Qi
AU - Gupta, Indranil
AU - Meseguer, José
N1 - Publisher Copyright:
© The Author(s) 2018.
PY - 2018
Y1 - 2018
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
Y2 - 16 April 2018 through 20 April 2018
ER -