{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T23:08:48Z","timestamp":1740179328975,"version":"3.37.3"},"reference-count":76,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2017,10,12]],"date-time":"2017-10-12T00:00:00Z","timestamp":1507766400000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/K008528"],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100003630","name":"Boeing","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100003630","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2017,10,12]]},"abstract":"Data replication is used in distributed systems to maintain up-to-date copies of shared data across multiple computers in a network. However, despite decades of research, algorithms for achieving consistency in replicated systems are still poorly understood. Indeed, many published algorithms have later been shown to be incorrect, even some that were accompanied by supposed mechanised proofs of correctness. In this work, we focus on the correctness of Conflict-free Replicated Data Types (CRDTs), a class of algorithm that provides strong eventual consistency guarantees for replicated data. We develop a modular and reusable framework in the Isabelle\/HOL interactive proof assistant for verifying the correctness of CRDT algorithms. We avoid correctness issues that have dogged previous mechanised proofs in this area by including a network model in our formalisation, and proving that our theorems hold in all possible network behaviours. Our axiomatic network model is a standard abstraction that accurately reflects the behaviour of real-world computer networks. Moreover, we identify an abstract convergence theorem, a property of order relations, which provides a formal definition of strong eventual consistency. We then obtain the first machine-checked correctness theorems for three concrete CRDTs: the Replicated Growable Array, the Observed-Remove Set, and an Increment-Decrement Counter. We find that our framework is highly reusable, developing proofs of correctness for the latter two CRDTs in a few hours and with relatively little CRDT-specific code.<\/jats:p>","DOI":"10.1145\/3133933","type":"journal-article","created":{"date-parts":[[2017,10,13]],"date-time":"2017-10-13T15:15:45Z","timestamp":1507907745000},"page":"1-28","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":33,"title":["Verifying strong eventual consistency in distributed systems"],"prefix":"10.1145","volume":"1","author":[{"given":"Victor B. F.","family":"Gomes","sequence":"first","affiliation":[{"name":"University of Cambridge, UK"}]},{"given":"Martin","family":"Kleppmann","sequence":"additional","affiliation":[{"name":"University of Cambridge, UK"}]},{"given":"Dominic P.","family":"Mulligan","sequence":"additional","affiliation":[{"name":"University of Cambridge, UK"}]},{"given":"Alastair R.","family":"Beresford","sequence":"additional","affiliation":[{"name":"University of Cambridge, UK"}]}],"member":"320","published-online":{"date-parts":[[2017,10,12]]},"reference":[{"key":"e_1_2_2_1_1","unstructured":"Akka 2017. The Akka actor framework for the Java Virtual Machine. (2017). http:\/\/www.akka.io\/ Accessed April 2017. Akka 2017. The Akka actor framework for the Java Virtual Machine. (2017). http:\/\/www.akka.io\/ Accessed April 2017."},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-26850-7_5"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-43652-3_9"},{"key":"e_1_2_2_4_1","unstructured":"AppJet Inc. 2011. Etherpad and EasySync Technical Manual. (March 2011). https:\/\/github.com\/ether\/etherpad-lite\/blob\/ e2ce9dc\/doc\/easysync\/easysync-full-description.pdf AppJet Inc. 2011. Etherpad and EasySync Technical Manual. (March 2011). https:\/\/github.com\/ether\/etherpad-lite\/blob\/ e2ce9dc\/doc\/easysync\/easysync-full-description.pdf"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933057.2933090"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2767386.2767419"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-33600-8_5"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2460276.2462076"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2639988.2639988"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2911151.2911159"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-43352-2_11"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33651-5_48"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2596631.2596633"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1561\/2500000011"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31057-7_14"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535848"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15260-3"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-24550-3_11"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/5505.5508"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/587078.587088"},{"key":"e_1_2_2_22_1","volume-title":"What\u2019s different about the new Google Docs: Making collaboration fast. (Sept","author":"Day-Richter John","year":"2010","unstructured":"John Day-Richter . 2010. What\u2019s different about the new Google Docs: Making collaboration fast. (Sept . 2010 ). https: \/\/drive.googleblog.com\/2010\/09\/whats-different-about-new-google-docs.html John Day-Richter. 2010. What\u2019s different about the new Google Docs: Making collaboration fast. (Sept. 2010). https: \/\/drive.googleblog.com\/2010\/09\/whats-different-about-new-google-docs.html"},{"key":"e_1_2_2_23_1","volume-title":"Verifying Fault-Tolerant Distributed Algorithms in the Heard-Of Model. Archive of Formal Proofs 2012","author":"Debrat Henri","year":"2012","unstructured":"Henri Debrat and Stephan Merz . 2012. Verifying Fault-Tolerant Distributed Algorithms in the Heard-Of Model. Archive of Formal Proofs 2012 ( 2012 ). https:\/\/www.isa-afp.org\/entries\/Heard_Of.shtml Henri Debrat and Stephan Merz. 2012. Verifying Fault-Tolerant Distributed Algorithms in the Heard-Of Model. Archive of Formal Proofs 2012 (2012). https:\/\/www.isa-afp.org\/entries\/Heard_Of.shtml"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1294261.1294281"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/67544.66963"},{"key":"e_1_2_2_26_1","volume-title":"11th Australian Computer Science Conference . 56\u201366","author":"Fidge Colin J","year":"1988","unstructured":"Colin J Fidge . 1988 . Timestamps in message-passing systems that preserve the partial ordering . In 11th Australian Computer Science Conference . 56\u201366 . Colin J Fidge. 1988. Timestamps in message-passing systems that preserve the partial ordering. In 11th Australian Computer Science Conference . 56\u201366."},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3064176.3064183"},{"key":"e_1_2_2_28_1","volume-title":"Beresford","author":"Gomes Victor B. F.","year":"2017","unstructured":"Victor B. F. Gomes , Martin Kleppmann , Dominic P. Mulligan , and Alastair R . Beresford . 2017 . A framework for establishing Strong Eventual Consistency for Conflict-free Replicated Datatypes. Archive of Formal Proofs (July 2017). http: \/\/isa-afp.org\/entries\/CRDT.shtml , Formal proof development. Victor B. F. Gomes, Martin Kleppmann, Dominic P. Mulligan, and Alastair R. Beresford. 2017. A framework for establishing Strong Eventual Consistency for Conflict-free Replicated Datatypes. Archive of Formal Proofs (July 2017). http: \/\/isa-afp.org\/entries\/CRDT.shtml , Formal proof development."},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12251-4_9"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02444-3_10"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-010-0068-0_17"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-010-0068-0_15"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.09.066"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2004.02.022"},{"key":"e_1_2_2_35_1","volume-title":"TP1-valid Transformation Functions for Operations on ordered n-ary Trees. arXiv:1512.05949. (Dec","author":"Jungnickel Tim","year":"2015","unstructured":"Tim Jungnickel and Tobias Herb . 2015. TP1-valid Transformation Functions for Operations on ordered n-ary Trees. arXiv:1512.05949. (Dec . 2015 ). https:\/\/arxiv.org\/abs\/1512.05949 Tim Jungnickel and Tobias Herb. 2015. TP1-valid Transformation Functions for Operations on ordered n-ary Trees. arXiv:1512.05949. (Dec. 2015). https:\/\/arxiv.org\/abs\/1512.05949"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48256-3_11"},{"key":"e_1_2_2_37_1","volume-title":"Jepsen: Cassandra. (Sept.","author":"Kingsbury Kyle","year":"2013","unstructured":"Kyle Kingsbury . 2013 . Jepsen: Cassandra. (Sept. 2013). https:\/\/aphyr.com\/posts\/294-jepsen-cassandra Accessed April 2017. Kyle Kingsbury. 2013. Jepsen: Cassandra. (Sept. 2013). https:\/\/aphyr.com\/posts\/294-jepsen-cassandra Accessed April 2017."},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1109\/TPDS.2017.2697382"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/359545.359563"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/DSN.2007.56"},{"key":"e_1_2_2_41_1","volume-title":"Towards a unified theory of Operational Transformation and CRDT. (July","author":"Levien Raph","year":"2016","unstructured":"Raph Levien . 2016. Towards a unified theory of Operational Transformation and CRDT. (July 2016 ). https:\/\/medium.com\/ @raphlinus\/towards-a-unified-theory-of-operational-transformation-and-crdt-70485876f72f Raph Levien. 2016. Towards a unified theory of Operational Transformation and CRDT. (July 2016). https:\/\/medium.com\/ @raphlinus\/towards-a-unified-theory-of-operational-transformation-and-crdt-70485876f72f"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/1031607.1031683"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10606-005-9009-5"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/1099203.1099252"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-16934-2_37"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/2790449.2790525"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/2872518.2890539"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/2494266.2494278"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/215585.215706"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10542-0"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1109\/COLCOM.2006.361867"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/1180875.1180916"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICDCS.2009.20"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2014.2308203"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1109\/2.485846"},{"key":"e_1_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/240080.240305"},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jpdc.2010.12.006"},{"key":"e_1_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF02277859"},{"key":"e_1_2_2_62_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-24550-3_29"},{"key":"e_1_2_2_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/2733108"},{"key":"e_1_2_2_64_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-43144-4_22"},{"key":"e_1_2_2_65_1","volume-title":"Understanding and Applying Operational Transformation. (May","author":"Spiewak Daniel","year":"2010","unstructured":"Daniel Spiewak . 2010. Understanding and Applying Operational Transformation. (May 2010 ). http:\/\/www.codecommit. com\/blog\/java\/understanding-and-applying-operational-transformation Daniel Spiewak. 2010. Understanding and Applying Operational Transformation. (May 2010). http:\/\/www.codecommit. com\/blog\/java\/understanding-and-applying-operational-transformation"},{"key":"e_1_2_2_66_1","doi-asserted-by":"publisher","DOI":"10.1145\/266838.267369"},{"key":"e_1_2_2_67_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICDE.1998.655755"},{"key":"e_1_2_2_68_1","doi-asserted-by":"publisher","DOI":"10.1145\/505151.505152"},{"key":"e_1_2_2_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/289444.289469"},{"key":"e_1_2_2_70_1","doi-asserted-by":"publisher","DOI":"10.1145\/274444.274447"},{"key":"e_1_2_2_71_1","doi-asserted-by":"publisher","DOI":"10.1109\/PDIS.1994.331722"},{"key":"e_1_2_2_72_1","doi-asserted-by":"publisher","DOI":"10.1109\/WETICE.2013.44"},{"key":"e_1_2_2_73_1","doi-asserted-by":"publisher","DOI":"10.1504\/IJAACS.2016.079623"},{"key":"e_1_2_2_74_1","doi-asserted-by":"publisher","DOI":"10.1145\/358916.358988"},{"key":"e_1_2_2_75_1","doi-asserted-by":"publisher","DOI":"10.1145\/1435417.1435432"},{"key":"e_1_2_2_76_1","volume-title":"Apache Software Foundation. (Aug","author":"Wang David","year":"2015","unstructured":"David Wang , Alex Mah , Soren Lassen , and Sam Thorogood . 2015. Apache Wave (incubating) Protocol Documentation , Release 0.4. Apache Software Foundation. (Aug . 2015 ). https:\/\/people.apache.org\/~al\/wave_docs\/ApacheWaveProtocol-0.4.pdf David Wang, Alex Mah, Soren Lassen, and Sam Thorogood. 2015. Apache Wave (incubating) Protocol Documentation, Release 0.4. Apache Software Foundation. (Aug. 2015). https:\/\/people.apache.org\/~al\/wave_docs\/ApacheWaveProtocol-0.4.pdf"},{"key":"e_1_2_2_77_1","doi-asserted-by":"publisher","DOI":"10.1109\/TPDS.2009.173"},{"key":"e_1_2_2_78_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_7"},{"key":"e_1_2_2_79_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737958"},{"key":"e_1_2_2_80_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-43613-4_3"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3133933","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,31]],"date-time":"2022-12-31T21:26:22Z","timestamp":1672521982000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3133933"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,10,12]]},"references-count":76,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2017,10,12]]}},"alternative-id":["10.1145\/3133933"],"URL":"https:\/\/doi.org\/10.1145\/3133933","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2017,10,12]]},"assertion":[{"value":"2017-10-12","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}