Read atomic transactions with prevention of lost updates: ROLA and its formal analysis
Tóm tắt
Designers of distributed database systems face the choice between stronger consistency guarantees and better performance. A number of applications only require read atomicity (RA) (either all or none of a transaction’s updates are visible to other transactions) and prevention of lost updates (PLU). Existing distributed transaction systems that meet these requirements also provide additional stronger consistency guarantees (such as causal consistency), but this comes at the price of lower performance. In this paper we propose a new distributed transaction protocol, ROLA, that targets application scenarios where only RA and PLU are needed. We formally specify 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) perform statistical model checking to analyze key performance properties; and (b) compare these performance results with those obtained by also modeling and analyzing in Maude the well-known protocols Walter and Jessy that also guarantee RA and PLU. Our statistical model checking results show that ROLA outperforms both Walter and Jessy.
Tài liệu tham khảo
Adya A (1999) Weak consistency: a generalized theory and optimistic implementations for distributed transactions. PhD thesis, MIT, Cambridge
AlTurki M, Meseguer J (2011) PVeStA: a parallel statistical model checking and quantitative analysis tool. In: CALCO'11, volume 6859 of LNCS. Springer, Berlin
Agha, G.A., Meseguer, J., Koushik, S.: PMaude: rewrite-based specification language for probabilistic object systems. Electr Notes Theor Comput Sci 153(2), 213–239 (2006)
Ardekani MS, Sutra P, Shapiro M (2013) Non-monotonic snapshot isolation: scalable and strong consistency for geo-replicated transactional systems. In: SRDS, IEEE Computer Society, pp 163–172
Baker J et al (2011) Megastore: providing scalable, highly available storage for interactive services. In: CIDR'11. www.cidrdb.org,
Benson T, Akella A, Maltz DA (2010) Network traffic characteristics of data centers in the wild. In: IMC, pp 267–280
Bailis P, Fekete A, Ghodsi A, Hellerstein JM, Stoica I (2016) Scalable atomic visibility with RAMP transactions. ACM Trans Database Syst, 41(3):15:1–15:45
Bailis P, Fekete A, Hellerstein JM, Ghodsi A, Stoica I (2014) Scalable atomic visibility with RAMP transactions. In: Proceeding of the SIGMOD'14. ACM
Bobba, R., Grov, J., Gupta, I., Liu, S., Meseguer, J., Ölveczky, P.C., Skeirik, S.: Survivability: design, formal modeling, and validation of cloud storage systems using Maude. In: Campbell, R.H., Kamhoua, C.A., Kwiat, K.A. (eds.) Assured cloud computing. Wiley-IEEE Computer Society Press, New Yok (2018)
Cerone A, Bernardi G, Gotsman A (2015) A framework for transactional consistency models with atomic visibility. In: CONCUR. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik
Clavel M, Durán F, Eker S, Lincoln P, Martí-Oliet N, Meseguer J, Talcott CL (2007) All about maude, volume 4350 of LNCS. Springer, Berlin
Cooper BF, Silberstein A, Tam E, Ramakrishnan R, Sears R (2010) Benchmarking cloud serving systems with YCSB. In: SOCC, pp 143–154
Eckhardt J, Mühlbauer T, Meseguer J, Wirsing M (2013) Statistical model checking for composite actor systems. In: WADT'12, volume 7841 of LNCS. Springer, Berlin
Grov J, Ölveczky PC (2014) Formal modeling and analysis of Google's Megastore in Real-Time Maude. In: Specification, algebra, and software, volume 8373 of LNCS. Springer, Berlin
Grov J, Ölveczky PC (2014) Increasing consistency in multi-site data stores: Megastore-CGC and its formal analysis. In: SEFM, volume 8702 of LNCS. Springer, Berlin
Hewitt, E.: Cassandra: the definitive guide. O'Reilly Media, Newton (2010)
Hawblitzel C, Howell J, Kapritsos M, Lorch JR, Parno B, Roberts ML, Setty STV, Zill B (2015) IronFleet: proving practical distributed systems correct. In: Proceedings of the 25th symposium on operating systems principles (SOSP'15). ACM, Cambridge
Liu S, Ganhotra J, Rahman M, Nguyen S, Gupta I, Meseguer J (2017) Quantitative analysis of consistency in NoSQL key-value stores. Leibniz Trans Embed Syst, 4(1):03:1–03:26
Leesatapornwongsa T, Hao M, Joshi P, Lukman JF, Gunawi HS (2014) SAMC: semantic-aware model checking for fast discovery of deep bugs in cloud systems. In: 11th USENIX symposium on operating systems design and implementation (OSDI'14). USENIX Association, Berkeley
Liu S, Nguyen S, Ganhotra J, Rahman MR, Gupta I, Meseguer J (2015) Quantitative analysis of consistency in NoSQL key-value stores. In: QEST, pp 228–243
Liu S, Ölveczky PC, Ganhotra J, Gupta I, Meseguer J (2017) Exploring design alternatives for RAMP transactions through statistical model checking. In: Proceedings of the ICFEM'17, volume 10610 of LNCS. Springer, Berlin
Liu S, Ölveczky PC, Rahman MR, Ganhotra J, Gupta I, Meseguer J (2016) Formal modeling and analysis of RAMP transaction systems. In: SAC'16. ACM, Cambridge
Liu, S., Ölveczky, P.C., Santhanam, K., Wang, Q., Gupta, I., Meseguer, J.: ROLA: a new distributed transaction protocol and its formal analysis. FASE, volume 10802 of LNCS, pp. 77–93. Springer, Berlin (2018)
Liu S, Ölveczky PC, Wang Q, Meseguer J (2018) Formal modeling and analysis of the Walter transactional data store. In: WRLA, volume 11152 of LNCS. Springer, Berlin
Liu, S., Ölveczky, P.C., Zhang, M., Wang, Q., Meseguer, J.: Automatic analysis of consistency properties of distributed transaction systems in Maude. TACAS'19, volume 11428 of LNCS, pp. 40–57. Springer, Berlin (2019)
Liu S, Rahman MR, Skeirik S, Gupta I, Meseguer J (2014) Formal modeling and analysis of Cassandra in Maude. In: ICFEM'14, volume 8829 of LNCS. Springer, Berlin
Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theoret Comput Sci 96(1), 73–155 (1992)
Meseguer J (1998) Membership algebra as a logical framework for equational specification. In: Proceedings of the WADT'97, volume 1376 of LNCS. Springer, Berlin
Meseguer J (2018) Formal design of cloud computing systems in Maude. Technical report, University of Illinois at Urbana-Champaign
Newcombe, C., Rath, T., Zhang, F., Munteanu, B., Brooker, M., Deardeuff, M.: How Amazon web services uses formal methods. Commun ACM 58(4), 66–73 (2015)
Ölveczky PC (2017) Formalizing and validating the P-Store replicated data store in Maude. In: Proceedings of the WADT'16, volume 10644 of Lecture Notes in Computer Science. Springer, Berlin
Ölveczky, P.C., Meseguer, J.: Semantics and pragmatics of real-time Maude. High Order Symb Comput 20(1–2), 161–196 (2007)
PRISM. http://www.prismmodelchecker.org/
Sovran Y, Power R, Aguilera MK, Li J (2011) Transactional storage for geo-replicated systems. In: SOSP 2011. ACM, Cambridge
Schiper N, Sutra P, Pedone F (2010) P-Store: genuine partial replication in wide area networks. In: Proceedings of the SRDS'10. IEEE Computer Society, New York
Sen K, Viswanathan M, Agha G (2005) On statistical model checking of stochastic systems. In: CAV'05, volume 3576 of LNCS. Springer, Berlin
Sen K, Viswanathan M, Agha GA (2005) VESTA: a statistical model-checker and analyzer for probabilistic systems. In: QEST'05. IEEE Computer Society, New York
Uppaal SMC. http://people.cs.aau.dk/~adavid/smc/
Yang J, Chen T, Wu M, Xu Z, Liu X, Lin H, Yang M, Long F, Zhang L, Zhou L (2009) MODIST: transparent model checking of unmodified distributed systems. In: Proceedings of the 6th USENIX symposium on networked systems design and implementation (NSDI'09),USENIX Association, pp 213–228
Younes, H.L.S., Simmons, R.G.: Statistical probabilistic model checking with a focus on time-bounded properties. Inf Comput 204(9), 1368–1409 (2006)
Zhang I, Sharma NK, Szekeres A, Krishnamurthy A, Ports DRK (2015) Building consistent transactions with inconsistent replication. In: Proceedings of the symposium on operating systems principles, (SOSP'15). ACM, 2015