{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T06:25:27Z","timestamp":1784183127110,"version":"3.55.0"},"reference-count":63,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2022,10,31]],"date-time":"2022-10-31T00:00:00Z","timestamp":1667174400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2022,10,31]]},"abstract":"<jats:p>Conflict-free replicated data types (CRDTs) are a promising tool for designing scalable, coordination-free distributed systems. However, constructing correct CRDTs is difficult, posing a challenge for even seasoned developers. As a result, CRDT development is still largely the domain of academics, with new designs often awaiting peer review and a manual proof of correctness. In this paper, we present Katara, a program synthesis-based system that takes sequential data type implementations and automatically synthesizes verified CRDT designs from them. Key to this process is a new formal definition of CRDT correctness that combines a reference sequential type with a lightweight ordering constraint that resolves conflicts between non-commutative operations. Our process follows the tradition of work in verified lifting, including an encoding of correctness into SMT logic using synthesized inductive invariants and hand-crafted grammars for the CRDT state and runtime. Katara is able to automatically synthesize CRDTs for a wide variety of scenarios, from reproducing classic CRDTs to synthesizing novel designs based on specifications in existing literature. Crucially, our synthesized CRDTs are fully, automatically verified, eliminating entire classes of common errors and reducing the process of producing a new CRDT from a painstaking paper proof of correctness to a lightweight specification.<\/jats:p>","DOI":"10.1145\/3563336","type":"journal-article","created":{"date-parts":[[2022,10,31]],"date-time":"2022-10-31T20:23:35Z","timestamp":1667247815000},"page":"1349-1377","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":19,"title":["Katara: synthesizing CRDTs with verified lifting"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6658-6548","authenticated-orcid":false,"given":"Shadaj","family":"Laddad","sequence":"first","affiliation":[{"name":"University of California at Berkeley, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0660-5110","authenticated-orcid":false,"given":"Conor","family":"Power","sequence":"additional","affiliation":[{"name":"University of California at Berkeley, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3126-7771","authenticated-orcid":false,"given":"Mae","family":"Milano","sequence":"additional","affiliation":[{"name":"University of California at Berkeley, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6261-6263","authenticated-orcid":false,"given":"Alvin","family":"Cheung","sequence":"additional","affiliation":[{"name":"University of California at Berkeley, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7712-4306","authenticated-orcid":false,"given":"Joseph M.","family":"Hellerstein","sequence":"additional","affiliation":[{"name":"University of California at Berkeley, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2022,10,31]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3183713.3196891"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3355089.3356549"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","unstructured":"Rajeev Alur Rastislav Bodik Garvit Juniwal Milo M. K. Martin Mukund Raghothaman Sanjit A. Seshia Rishabh Singh Armando Solar-Lezama Emina Torlak and Abhishek Udupa. 2013. Syntax-guided synthesis. In 2013 Formal Methods in Computer-Aided Design. 1\u20138. https:\/\/doi.org\/10.1109\/FMCAD.2013.6679385 10.1109\/FMCAD.2013.6679385","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICDE.2014.6816639"},{"key":"e_1_2_1_5_1","unstructured":"Peter Alvaro Neil Conway Joseph M Hellerstein and William R Marczak. 2011. Consistency Analysis in Bloom: a CALM and Collected Approach.. In CIDR. 249\u2013260."},{"key":"e_1_2_1_6_1","volume-title":"Dedalus: Datalog in time and space. In International Datalog 2.0 Workshop. 262\u2013281.","author":"Alvaro Peter","year":"2010","unstructured":"Peter Alvaro, William R Marczak, Neil Conway, Joseph M Hellerstein, David Maier, and Russell Sears. 2010. Dedalus: Datalog in time and space. In International Datalog 2.0 Workshop. 262\u2013281."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.14778\/3297753.3297760"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2741948.2741972"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"e_1_2_1_10_1","volume-title":"Cloud Types for Eventual Consistency. In ECOOP 2012 \u2013 Object-Oriented Programming, James Noble (Ed.). Springer Berlin Heidelberg","author":"Burckhardt Sebastian","unstructured":"Sebastian Burckhardt, Manuel F\u00e4hndrich, Daan Leijen, and Benjamin P. Wood. 2012. Cloud Types for Eventual Consistency. In ECOOP 2012 \u2013 Object-Oriented Programming, James Noble (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 283\u2013307. isbn:978-3-642-31057-7"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2578855.2535848"},{"key":"e_1_2_1_12_1","volume-title":"The Conference on Innovative Data Systems Research (CIDR), 14 pages.","author":"Cheung Alvin","year":"2021","unstructured":"Alvin Cheung, Natacha Crooks, Joseph M Hellerstein, and Mae Milano. 2021. New directions in cloud programming. The Conference on Innovative Data Systems Research (CIDR), 14 pages."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462180"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.14778\/2732279.2732285"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2391229.2391230"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2882903.2882951"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485484"},{"key":"e_1_2_1_19_1","volume-title":"Christophe Scholliers, Wolfgang De Meuter, and Elisa Gonzalez Boix.","author":"Porre Kevin De","year":"2019","unstructured":"Kevin De Porre, Florian Myter, Christophe De Troyer, Christophe Scholliers, Wolfgang De Meuter, and Elisa Gonzalez Boix. 2019. Putting Order in Strong Eventual Consistency. In Distributed Applications and Interoperable Systems, Jos\u00e9 Pereira and Laura Ricci (Eds.). Springer International Publishing, Cham. 36\u201356. isbn:978-3-030-22496-7"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jpdc.2020.05.010"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1294261.1294281"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/41840.41841"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133933"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837625"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3369736"},{"key":"e_1_2_1_26_1","unstructured":"Todd Hoff. 2014. How League Of Legends Scaled Chat To 70 Million Players - It Takes Lots Of Minions. http:\/\/highscalability.com\/blog\/2014\/10\/13\/how-league-of-legends-scaled-chat-to-70-million-players-it-t.html"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2987550.2987559"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290387"},{"key":"e_1_2_1_29_1","volume-title":"Proceedings of the 2010 USENIX Conference on USENIX Annual Technical Conference (USENIXATC\u201910)","author":"Hunt Patrick","year":"2010","unstructured":"Patrick Hunt, Mahadev Konar, Flavio P. Junqueira, and Benjamin Reed. 2010. ZooKeeper: Wait-Free Coordination for Internet-Scale Systems. In Proceedings of the 2010 USENIX Conference on USENIX Annual Technical Conference (USENIXATC\u201910). USENIX Association, USA. 11."},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276534"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360580"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2980983.2908117"},{"key":"e_1_2_1_33_1","unstructured":"Martin Kleppmann. 2018. Data structures as queries: Expressing CRDTs using Datalog. https:\/\/martin.kleppmann.com\/2018\/02\/26\/dagstuhl-data-consistency.html"},{"key":"e_1_2_1_34_1","volume-title":"Assessing the understandability of a distributed algorithm by tweeting buggy pseudocode","author":"Kleppmann Martin","unstructured":"Martin Kleppmann. 2022. Assessing the understandability of a distributed algorithm by tweeting buggy pseudocode. University of Cambridge, Computer Laboratory."},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/TPDS.2017.2697382"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/1900160.1900176"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2502323.2502326"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1773912.1773922"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/359545.359563"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/279227.279229"},{"key":"e_1_2_1_41_1","volume-title":"Automating the Choice of Consistency Levels in Replicated Systems. In 2014 USENIX Annual Technical Conference (USENIX ATC 14)","author":"Li Cheng","year":"2014","unstructured":"Cheng Li, Joao Leit\u00e3o, Allen Clement, Nuno Pregui\u00e7a, Rodrigo Rodrigues, and Viktor Vafeiadis. 2014. Automating the Choice of Consistency Levels in Replicated Systems. In 2014 USENIX Annual Technical Conference (USENIX ATC 14). USENIX Association, Philadelphia, PA. 281\u2013292. isbn:978-1-931971-10-2 https:\/\/www.usenix.org\/conference\/atc14\/technical-sessions\/presentation\/li_cheng_2"},{"key":"e_1_2_1_42_1","volume-title":"10th USENIX Symposium on Operating Systems Design and Implementation (OSDI 12)","author":"Li Cheng","year":"2012","unstructured":"Cheng Li, Daniel Porto, Allen Clement, Johannes Gehrke, Nuno Pregui\u00e7a, and Rodrigo Rodrigues. 2012. Making Geo-Replicated Systems Fast as Possible, Consistent when Necessary. In 10th USENIX Symposium on Operating Systems Design and Implementation (OSDI 12). USENIX Association, Hollywood, CA. 265\u2013278. isbn:978-1-931971-96-6 https:\/\/www.usenix.org\/conference\/osdi12\/technical-sessions\/presentation\/li"},{"key":"e_1_2_1_43_1","volume-title":"Hampa: Solver-Aided Recency-Aware Replication","author":"Li Xiao","year":"2020","unstructured":"Xiao Li, Farzin Houshmand, and Mohsen Lesani. 2020. Hampa: Solver-Aided Recency-Aware Replication. In Computer Aided Verification, Shuvendu K. Lahiri and Chao Wang (Eds.). Springer International Publishing, Cham. 324\u2013349. isbn:978-3-030-53288-8"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428284"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/2790449.2790525"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192375"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.SNAPL.2019.11"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","unstructured":"Kartik Nagar and Suresh Jagannathan. 2019. Automated Parameterized Verification of CRDTs. https:\/\/doi.org\/10.48550\/ARXIV.1905.05684","DOI":"10.48550\/ARXIV.1905.05684"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.5555\/2643634.2643666"},{"key":"e_1_2_1_50_1","volume-title":"Akka in action","author":"Roestenburg Raymond","unstructured":"Raymond Roestenburg, Rob Williams, and Robertus Bakker. 2016. Akka in action. Simon and Schuster."},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-24550-3_29"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737981"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/2934872.2934900"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/3358499.3361222"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523735"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509578.2509586"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/1435417.1435432"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314617"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICDCS.2009.75"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICDE.2018.00044"},{"key":"e_1_2_1_62_1","volume-title":"Formal Techniques for Distributed Objects, Components, and Systems, Erika \u00c1brah\u00e1m and Catuscia Palamidessi (Eds.)","author":"Zeller Peter","unstructured":"Peter Zeller, Annette Bieniusa, and Arnd Poetzsch-Heffter. 2014. Formal Specification and Verification of CRDTs. In Formal Techniques for Distributed Objects, Components, and Systems, Erika \u00c1brah\u00e1m and Catuscia Palamidessi (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 33\u201348. isbn:978-3-662-43613-4"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/3281366.3281372"},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2020.100561"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3563336","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3563336","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:38:10Z","timestamp":1750178290000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3563336"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,10,31]]},"references-count":63,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2022,10,31]]}},"alternative-id":["10.1145\/3563336"],"URL":"https:\/\/doi.org\/10.1145\/3563336","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,10,31]]},"assertion":[{"value":"2022-10-31","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}