{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,18]],"date-time":"2026-03-18T21:15:44Z","timestamp":1773868544575,"version":"3.50.1"},"reference-count":40,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2019,10,10]],"date-time":"2019-10-10T00:00:00Z","timestamp":1570665600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF-SHF 1717741"],"award-info":[{"award-number":["CCF-SHF 1717741"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100006602","name":"Air Force Research Laboratory","doi-asserted-by":"publisher","award":["FA8750-17-1-0006"],"award-info":[{"award-number":["FA8750-17-1-0006"]}],"id":[{"id":"10.13039\/100006602","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":[[2019,10,10]]},"abstract":"<jats:p>Programming geo-replicated distributed systems is challenging given the complexity of reasoning about different evolving states on different replicas. Existing approaches to this problem impose significant burden on application developers to consider the effect of how operations performed on one replica are witnessed and applied on others. To alleviate these challenges, we present a fundamentally different approach to programming in the presence of replicated state. Our insight is based on the use of invertible relational specifications of an inductively-defined data type as a mechanism to capture salient aspects of the data type relevant to how its different instances can be safely merged in a replicated environment. Importantly, because these specifications only address a data type's (static) structural properties, their formulation does not require exposing low-level system-level details concerning asynchrony, replication, visibility, etc. As a consequence, our framework enables the correct-by-construction synthesis of rich merge functions over arbitrarily complex (i.e., composable) data types. We show that the use of a rich relational specification language allows us to extract sufficient conditions to automatically derive merge functions that have meaningful non-trivial convergence properties. We incorporate these ideas in a tool called Quark, and demonstrate its utility via a detailed evaluation study on real-world benchmarks.<\/jats:p>","DOI":"10.1145\/3360580","type":"journal-article","created":{"date-parts":[[2019,10,11]],"date-time":"2019-10-11T14:53:33Z","timestamp":1570805613000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":25,"title":["Mergeable replicated data types"],"prefix":"10.1145","volume":"3","author":[{"given":"Gowtham","family":"Kaki","sequence":"first","affiliation":[{"name":"Purdue University, USA"}]},{"given":"Swarn","family":"Priya","sequence":"additional","affiliation":[{"name":"Purdue University, USA"}]},{"given":"KC","family":"Sivaramakrishnan","sequence":"additional","affiliation":[{"name":"IIT Madras, India"}]},{"given":"Suresh","family":"Jagannathan","sequence":"additional","affiliation":[{"name":"Purdue University, USA"}]}],"member":"320","published-online":{"date-parts":[[2019,10,10]]},"reference":[{"key":"e_1_2_2_1_1","volume-title":"CIDR 2011, Fifth Biennial Conference on Innovative Data Systems Research, Asilomar, CA, USA, January 9-12, 2011, Online Proceedings. 249\u2013260","author":"Alvaro Peter","unstructured":"Peter Alvaro , Neil Conway , Joe Hellerstein , and William R. Marczak . 2011. Consistency Analysis in Bloom: a CALM and Collected Approach . In CIDR 2011, Fifth Biennial Conference on Innovative Data Systems Research, Asilomar, CA, USA, January 9-12, 2011, Online Proceedings. 249\u2013260 . Peter Alvaro, Neil Conway, Joe Hellerstein, and William R. Marczak. 2011. Consistency Analysis in Bloom: a CALM and Collected Approach. In CIDR 2011, Fifth Biennial Conference on Innovative Data Systems Research, Asilomar, CA, USA, January 9-12, 2011, Online Proceedings. 249\u2013260."},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.14778\/2732232.2732237"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.14778\/2735508.2735509"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2463676.2465279"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2741948.2741972"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1002\/spe.4380251203"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/800177.810020"},{"key":"e_1_2_2_8_1","unstructured":"Brewer 2013. (2013). http:\/\/highscalability.com\/blog\/2013\/5\/1\/myth- eric- brewer- on- why- banks- are- base- not- acidavailability.html Myth: Eric Brewer on Why Banks are BASE Not ACID - Availability Is Revenue.  Brewer 2013. (2013). http:\/\/highscalability.com\/blog\/2013\/5\/1\/myth- eric- brewer- on- why- banks- are- base- not- acidavailability.html Myth: Eric Brewer on Why Banks are BASE Not ACID - Availability Is Revenue."},{"key":"e_1_2_2_9_1","doi-asserted-by":"crossref","unstructured":"Eric Brewer. 2000. Towards Robust Distributed Systems (Invited Talk). (2000).  Eric Brewer. 2000. Towards Robust Distributed Systems (Invited Talk). (2000).","DOI":"10.1145\/343477.343502"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1869459.1869515"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31057-7_14"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535848"},{"key":"e_1_2_2_13_1","volume-title":"Proceedings of the 29th European Conference on Object-Oriented Programming (ECOOP \u201915)","author":"Burckhardt Sebastian","year":"2015","unstructured":"Sebastian Burckhardt , Daan Leijen , Jonathan Protzenko , and Manuel F\u00e4hndrich . 2015 . Global Sequence Protocol: A Robust Abstraction for Replicated Shared State . In Proceedings of the 29th European Conference on Object-Oriented Programming (ECOOP \u201915) . Prague, Czech Republic. http:\/\/research.microsoft.com\/pubs\/240462\/gsp- tr- 2015- 2.pdf Sebastian Burckhardt, Daan Leijen, Jonathan Protzenko, and Manuel F\u00e4hndrich. 2015. Global Sequence Protocol: A Robust Abstraction for Replicated Shared State. In Proceedings of the 29th European Conference on Object-Oriented Programming (ECOOP \u201915). Prague, Czech Republic. http:\/\/research.microsoft.com\/pubs\/240462\/gsp- tr- 2015- 2.pdf"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328469"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2882903.2882951"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796801004075"},{"key":"e_1_2_2_17_1","unstructured":"Functional Graph 2008. A Functional Graph Library. (2008). http:\/\/hackage.haskell.org\/package\/fgl  Functional Graph 2008. A Functional Graph Library. (2008). http:\/\/hackage.haskell.org\/package\/fgl"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837625"},{"key":"e_1_2_2_19_1","volume-title":"Hamsaz: Replication Coordination Analysis and Synthesis. PACMPL 3, POPL","author":"Houshmand Farzin","year":"2019","unstructured":"Farzin Houshmand and Mohsen Lesani . 2019 . Hamsaz: Replication Coordination Analysis and Synthesis. PACMPL 3, POPL (2019), 74:1\u201374:32. https:\/\/dl.acm.org\/citation.cfm?id=3290387 Farzin Houshmand and Mohsen Lesani. 2019. Hamsaz: Replication Coordination Analysis and Synthesis. PACMPL 3, POPL (2019), 74:1\u201374:32. https:\/\/dl.acm.org\/citation.cfm?id=3290387"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1667048.1667050"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796801004026"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628159"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158115"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.SNAPL.2019.8"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837622"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.5555\/2643634.2643664"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.5555\/2643634.2643664"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.5555\/2387880.2387906"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.5555\/2387880.2387906"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3191315.3191317"},{"key":"e_1_2_2_31_1","volume-title":"Purely Functional Data Structures","author":"Okasaki Chris","unstructured":"Chris Okasaki . 1998. Purely Functional Data Structures . Cambridge University Press , New York, NY, USA . Chris Okasaki. 1998. Purely Functional Data Structures. Cambridge University Press, New York, NY, USA."},{"key":"e_1_2_2_32_1","unstructured":"PPX 2017. PPX extension points. (2017). Accessed: 2017-01-04 10:12:00.  PPX 2017. PPX extension points. (2017). Accessed: 2017-01-04 10:12:00."},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICDCS.2009.20"},{"key":"e_1_2_2_34_1","unstructured":"RUBiS 2014. Rice University Bidding System. (2014). http:\/\/rubis.ow2.org\/ Accessed: 2014-11-4 13:21:00.  RUBiS 2014. Rice University Bidding System. (2014). http:\/\/rubis.ow2.org\/ Accessed: 2014-11-4 13:21:00."},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-24550-3_29"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-24550-3_29"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737981"},{"key":"e_1_2_2_38_1","unstructured":"TPC 2018. (2018). http:\/\/www.tpc.org\/information\/benchmarks.asp TPC Benchmarks.  TPC 2018. (2018). http:\/\/www.tpc.org\/information\/benchmarks.asp TPC Benchmarks."},{"key":"e_1_2_2_39_1","unstructured":"Twissandra 2014. Twitter clone on Cassandra. (2014). http:\/\/twissandra.com\/ Accessed: 2014-11-4 13:21:00.  Twissandra 2014. Twitter clone on Cassandra. (2014). http:\/\/twissandra.com\/ Accessed: 2014-11-4 13:21:00."},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737958"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3360580","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3360580","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3360580","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:22:59Z","timestamp":1750202579000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3360580"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,10,10]]},"references-count":40,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2019,10,10]]}},"alternative-id":["10.1145\/3360580"],"URL":"https:\/\/doi.org\/10.1145\/3360580","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,10,10]]},"assertion":[{"value":"2019-10-10","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}