{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,23]],"date-time":"2026-08-23T17:51:15Z","timestamp":1787507475337,"version":"build-2736575974"},"reference-count":41,"publisher":"Association for Computing Machinery (ACM)","issue":"5","license":[{"start":{"date-parts":[[2019,11,1]],"date-time":"2019-11-01T00:00:00Z","timestamp":1572566400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2019,11,1]],"date-time":"2019-11-01T00:00:00Z","timestamp":1572566400000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2019,11]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    Designers of distributed database systems face the choice between stronger consistency guarantees and better performance. A number of applications only require\n                    <jats:italic>read atomicity<\/jats:italic>\n                    (RA) (either all or none of a transaction\u2019s updates are visible to other transactions) and\n                    <jats:italic>prevention of lost updates<\/jats:italic>\n                    (PLU). Existing distributed transaction systems that meet these requirements also provide additional stronger consistency guarantees (such as\n                    <jats:italic>causal consistency<\/jats:italic>\n                    ), 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\u2019s satisfaction of RA and PLU. To analyze\n                    <jats:italic>performance<\/jats:italic>\n                    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.\n                  <\/jats:p>","DOI":"10.1007\/s00165-019-00489-w","type":"journal-article","created":{"date-parts":[[2019,8,2]],"date-time":"2019-08-02T06:50:44Z","timestamp":1564728644000},"page":"503-540","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":17,"title":["Read atomic transactions with prevention of lost updates: ROLA and its formal analysis"],"prefix":"10.1145","volume":"31","author":[{"given":"Si","family":"Liu","sequence":"first","affiliation":[{"name":"University of Illinois, Urbana-Champaign, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Peter Csaba","family":"\u00d6lveczky","sequence":"additional","affiliation":[{"name":"University of Oslo, Oslo, Norway"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Qi","family":"Wang","sequence":"additional","affiliation":[{"name":"University of Illinois, Urbana-Champaign, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Indranil","family":"Gupta","sequence":"additional","affiliation":[{"name":"University of Illinois, Urbana-Champaign, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jos\u00e9","family":"Meseguer","sequence":"additional","affiliation":[{"name":"University of Illinois, Urbana-Champaign, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","unstructured":"Adya A (1999) Weak consistency: a generalized theory and optimistic implementations for distributed transactions. PhD thesis MIT Cambridge"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"AlTurki M Meseguer J (2011) PVeStA: a parallel statistical model checking and quantitative analysis tool. In: CALCO'11 volume 6859 of LNCS. Springer Berlin","DOI":"10.1007\/978-3-642-22944-2_28"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.10.040"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"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\u2013172","DOI":"10.1109\/SRDS.2013.25"},{"key":"e_1_2_1_2_5_2","unstructured":"Baker J et\u00a0al (2011) Megastore: providing scalable highly available storage for interactive services. In: CIDR'11. www.cidrdb.org"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Benson T Akella A Maltz DA (2010) Network traffic characteristics of data centers in the wild. In: IMC pp 267\u2013280","DOI":"10.1145\/1879141.1879175"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"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\u201315:45","DOI":"10.1145\/2909870"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Bailis P Fekete A Hellerstein JM Ghodsi A Stoica I (2014) Scalable atomic visibility with RAMP transactions. In: Proceeding of the SIGMOD'14. ACM","DOI":"10.1145\/2588555.2588562"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"publisher","DOI":"10.1002\/9781119428497.ch2"},{"key":"e_1_2_1_2_10_2","unstructured":"Cerone A Bernardi G Gotsman A (2015) A framework for transactional consistency models with atomic visibility. In:  CONCUR. Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik"},{"key":"e_1_2_1_2_11_2","unstructured":"Clavel M Dur\u00e1n F Eker S Lincoln P Mart\u00ed-Oliet N Meseguer J Talcott CL (2007) All about maude volume 4350 of LNCS. Springer Berlin"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Cooper BF Silberstein A Tam E Ramakrishnan R Sears R (2010) Benchmarking cloud serving systems with YCSB. In: SOCC pp 143\u2013154","DOI":"10.1145\/1807128.1807152"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Eckhardt J M\u00fchlbauer T Meseguer J Wirsing M (2013) Statistical model checking for composite actor systems. In: WADT'12 volume 7841 of LNCS. Springer Berlin","DOI":"10.1007\/978-3-642-37635-1_9"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"Grov J \u00d6lveczky 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","DOI":"10.1007\/978-3-642-54624-2_25"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Grov J \u00d6lveczky PC (2014) Increasing consistency in multi-site data stores: Megastore-CGC and its formal analysis. In: SEFM volume 8702 of LNCS. Springer Berlin","DOI":"10.1007\/978-3-319-10431-7_12"},{"key":"e_1_2_1_2_16_2","volume-title":"Cassandra: the definitive guide","author":"Hewitt E","year":"2010"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"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","DOI":"10.1145\/2815400.2815428"},{"key":"e_1_2_1_2_18_2","unstructured":"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\u201303:26"},{"key":"e_1_2_1_2_19_2","unstructured":"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"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"crossref","unstructured":"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\u2013243","DOI":"10.1007\/978-3-319-22264-6_15"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"Liu S \u00d6lveczky 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","DOI":"10.1007\/978-3-319-68690-5_18"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"crossref","unstructured":"Liu S \u00d6lveczky PC Rahman MR Ganhotra J Gupta I Meseguer J (2016) Formal modeling and analysis of RAMP transaction systems. In: SAC'16. ACM Cambridge","DOI":"10.1145\/2851613.2851838"},{"key":"e_1_2_1_2_23_2","first-page":"77","volume-title":"FASE, volume 10802 of LNCS","author":"Liu S","year":"2018"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"crossref","unstructured":"Liu S \u00d6lveczky PC Wang Q Meseguer J (2018) Formal modeling and analysis of the Walter transactional data store. In: WRLA volume 11152 of LNCS. Springer Berlin","DOI":"10.1007\/978-3-319-99840-4_8"},{"key":"e_1_2_1_2_25_2","first-page":"40","volume-title":"TACAS'19, volume 11428 of LNCS","author":"Liu S","year":"2019"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"crossref","unstructured":"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","DOI":"10.1007\/978-3-319-11737-9_22"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90182-F"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"crossref","unstructured":"Meseguer J (1998) Membership algebra as a logical framework for equational specification. In: Proceedings of the WADT'97 volume 1376 of LNCS. Springer Berlin","DOI":"10.1007\/3-540-64299-4_26"},{"key":"e_1_2_1_2_29_2","unstructured":"Meseguer J (2018) Formal design of cloud computing systems in Maude. Technical report University of Illinois at Urbana-Champaign"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"publisher","DOI":"10.1145\/2699417"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"crossref","unstructured":"\u00d6lveczky 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","DOI":"10.1007\/978-3-319-72044-9_13"},{"issue":"1","key":"e_1_2_1_2_32_2","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1007\/s10990-007-9001-5","article-title":"Semantics and pragmatics of real-time Maude","volume":"20","author":"\u00d6lveczky PC","year":"2007","journal-title":"High Order Symb Comput"},{"key":"e_1_2_1_2_33_2","unstructured":"PRISM. http:\/\/www.prismmodelchecker.org\/"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"crossref","unstructured":"Sovran Y Power R Aguilera MK Li J (2011) Transactional storage for geo-replicated systems. In: SOSP 2011. ACM Cambridge","DOI":"10.1145\/2043556.2043592"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"crossref","unstructured":"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","DOI":"10.1109\/SRDS.2010.32"},{"key":"e_1_2_1_2_36_2","doi-asserted-by":"crossref","unstructured":"Sen K Viswanathan M Agha G (2005) On statistical model checking of stochastic systems. In: CAV'05 volume 3576 of LNCS. Springer Berlin","DOI":"10.1007\/11513988_26"},{"key":"e_1_2_1_2_37_2","doi-asserted-by":"crossref","unstructured":"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","DOI":"10.1109\/QEST.2005.42"},{"key":"e_1_2_1_2_38_2","unstructured":"Uppaal SMC. http:\/\/people.cs.aau.dk\/~adavid\/smc\/"},{"key":"e_1_2_1_2_39_2","unstructured":"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\u2013228"},{"key":"e_1_2_1_2_40_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2006.05.002"},{"key":"e_1_2_1_2_41_2","doi-asserted-by":"crossref","unstructured":"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","DOI":"10.1145\/2815400.2815404"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-019-00489-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-019-00489-w\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-019-00489-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-019-00489-w","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T11:12:25Z","timestamp":1641467545000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-019-00489-w"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,11]]},"references-count":41,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2019,11]]}},"alternative-id":["10.1007\/s00165-019-00489-w"],"URL":"https:\/\/doi.org\/10.1007\/s00165-019-00489-w","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,11]]},"assertion":[{"value":"30 September 2018","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"12 July 2019","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"2 August 2019","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}