{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T01:07:44Z","timestamp":1760058464699,"version":"build-2065373602"},"reference-count":29,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA1","license":[{"start":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T00:00:00Z","timestamp":1744156800000},"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":[[2025,4,9]]},"abstract":"<jats:p>Data replication is crucial for enabling fault tolerance and uniform low latency in modern decentralized applications. Replicated Data Types (RDTs) have emerged as a principled approach for developing replicated implementations of basic data structures such as counter, flag, set, map, etc. While the correctness of RDTs is generally specified using the notion of strong eventual consistency--which guarantees that replicas that have received the same set of updates would converge to the same state--a more expressive specification which relates the converged state to updates received at a replica would be more beneficial to RDT users. Replication-aware linearizability is one such specification, which requires all replicas to always be in a state which can be obtained by linearizing the updates received at the replica. In this work, we develop a novel fully automated technique for verifying replication-aware linearizability for Mergeable Replicated Data Types (MRDTs). We identify novel algebraic properties for MRDT operations and the merge function which are sufficient for proving an implementation to be linearizable and which go beyond the standard notions of commutativity, associativity, and idempotence. We also develop a novel inductive technique called bottom-up linearization to automatically verify the required algebraic properties. Our technique can be used to verify both MRDTs and state-based CRDTs. We have successfully applied our approach to a number of complex MRDT and CRDT implementations including a novel JSON MRDT.<\/jats:p>","DOI":"10.1145\/3720452","type":"journal-article","created":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T13:48:26Z","timestamp":1744206506000},"page":"871-897","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Automatically Verifying Replication-Aware Linearizability"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9987-7491","authenticated-orcid":false,"given":"Vimala","family":"Soundarapandian","sequence":"first","affiliation":[{"name":"IIT Madras, Chennai, India"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0679-226X","authenticated-orcid":false,"given":"Kartik","family":"Nagar","sequence":"additional","affiliation":[{"name":"IIT Madras, Chennai, India"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3283-8011","authenticated-orcid":false,"given":"Aseem","family":"Rastogi","sequence":"additional","affiliation":[{"name":"Microsoft Research, Bangalore, India"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3491-1780","authenticated-orcid":false,"given":"KC","family":"Sivaramakrishnan","sequence":"additional","affiliation":[{"name":"IIT Madras, Chennai, India"},{"name":"Tarides, Chennai, India"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,4,9]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933057.2933090"},{"key":"e_1_2_1_2_1","unstructured":"Automerge. 2022. Automerge. https:\/\/automerge.org\/"},{"key":"e_1_2_1_3_1","volume-title":"An optimized conflict-free replicated set. CoRR, abs\/1210.3368","author":"Bieniusa Annette","year":"2012","unstructured":"Annette Bieniusa, Marek Zawirski, Nuno M. Pregui\u00e7a, Marc Shapiro, Carlos Baquero, Valter Balegas, and S\u00e9rgio Duarte. 2012. An optimized conflict-free replicated set. CoRR, abs\/1210.3368 (2012), arXiv:1210.3368. arxiv:1210.3368"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535848"},{"key":"e_1_2_1_5_1","volume-title":"Gustavo Petri, and Chao Wang.","author":"Enea Constantin","year":"2019","unstructured":"Constantin Enea, Suha Orhun Mutluergil, Gustavo Petri, and Chao Wang. 2019. Replication-Aware Linearizability. CoRR, abs\/1903.06560 (2019), arXiv:1903.06560. arxiv:1903.06560"},{"volume-title":"Git: A distributed version control system. https:\/\/git-scm.com\/","year":"2021","key":"e_1_2_1_6_1","unstructured":"Git. 2021. Git: A distributed version control system. https:\/\/git-scm.com\/"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133933"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837625"},{"volume-title":"Irmin: A distributed database built on the principles of Git. https:\/\/irmin.org\/","year":"2021","key":"e_1_2_1_9_1","unstructured":"Irmin. 2021. Irmin: A distributed database built on the principles of Git. https:\/\/irmin.org\/"},{"key":"e_1_2_1_10_1","unstructured":"Json. [n. d.]. Json: A lightweight data-interchange format. https:\/\/www.json.org\/"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523724"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360580"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563336"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/359545.359563"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428284"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25543-5_26"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-44914-8_20"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ECOOP.2023.9"},{"key":"e_1_2_1_19_1","unstructured":"Riak. 2021. Resilient NoSQL Databases. https:\/\/riak.com\/"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jpdc.2010.12.006"},{"volume-title":"A comprehensive study of Convergent and Commutative Replicated Data Types. Inria \u2013 Centre Paris-Rocquencourt","author":"Shapiro Marc","key":"e_1_2_1_21_1","unstructured":"Marc Shapiro, Nuno Pregui\u00e7a, Carlos Baquero, and Marek Zawirski. 2011. A comprehensive study of Convergent and Commutative Replicated Data Types. Inria \u2013 Centre Paris-Rocquencourt ; INRIA, 50. https:\/\/inria.hal.science\/inria-00555588"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-24550-3_29"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523735"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","unstructured":"Vimala Soundarapandian Kartik Nagar Aseem Rastogi and KC Sivaramakrishnan. 2025. Automatically Verifying Replication-aware Linearizability (Artifact). https:\/\/doi.org\/10.5281\/zenodo.14922118 10.5281\/zenodo.14922118","DOI":"10.5281\/zenodo.14922118"},{"key":"e_1_2_1_25_1","unstructured":"Vimala Soundarapandian Kartik Nagar Aseem Rastogi and KC Sivaramakrishnan. 2025. Automatically Verifying Replication-aware Linearizability (Extended version). arxiv:2502.19967. arxiv:2502.19967"},{"key":"e_1_2_1_26_1","doi-asserted-by":"crossref","unstructured":"Vimala Soundarapandian Kartik Nagar Aseem Rastogi and KC Sivaramakrishnan. 2025. Automatically Verifying Replication-aware Linearizability (GitHub Repository). https:\/\/github.com\/prismlab\/certified-mrdts","DOI":"10.1145\/3720452"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2914770.2837655"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314617"},{"key":"e_1_2_1_29_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\/10.1145\/3720452","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3720452","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T17:06:58Z","timestamp":1760029618000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3720452"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,4,9]]},"references-count":29,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2025,4,9]]}},"alternative-id":["10.1145\/3720452"],"URL":"https:\/\/doi.org\/10.1145\/3720452","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2025,4,9]]},"assertion":[{"value":"2024-10-15","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-02-18","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-04-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}