{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,23]],"date-time":"2026-09-23T17:08:11Z","timestamp":1790183291450,"version":"4.1.0"},"reference-count":44,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2018,10,24]],"date-time":"2018-10-24T00:00:00Z","timestamp":1540339200000},"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":[[2018,10,24]]},"abstract":"<jats:p>High-level data types are often associated with semantic invariants that must be preserved by any correct implementation. While having implementations enforce strong guarantees such as linearizability or serializability can often be used to prevent invariant violations in concurrent settings, such mechanisms are impractical in geo-distributed replicated environments, the platform of choice for many scalable Web services. To achieve high-availability essential to this domain, these environments admit various forms of weak consistency that do not guarantee all replicas have a consistent view of an application's state. Consequently, they often admit difficult-to-understand anomalous behaviors that violate a data type's invariants, but which are extremely challenging, even for experts, to understand and debug.<\/jats:p>\n          <jats:p>In this paper, we propose a novel programming framework for replicated data types (RDTs) equipped with an automatic (bounded) verification technique that discovers and fixes weak consistency anomalies. Our approach, implemented in a tool called Q9, involves systematically exploring the state space of an application executing on top of an eventually consistent data store, under an unrestricted consistency model but with a finite concurrency bound. Q9 uncovers anomalies (i.e., invariant violations) that manifest as finite counterexamples, and automatically generates repairs for such anamolies by selectively strengthening consistency guarantees for specific operations. Using Q9, we have uncovered a range of subtle anomalies in implementations of well-known benchmarks, and have been able to apply the repairs it mandates to effectively eliminate them. Notably, these benchmarks were written adopting best practices suggested to manage distributed replicated state (e.g., they are composed of provably convergent RDTs (CRDTs), avoid mutable state, etc.). While the safety guarantees offered by our technique are constrained by the concurrency bound, we show that in practice, proving bounded safety guarantees typically generalize to the unbounded case.<\/jats:p>","DOI":"10.1145\/3276534","type":"journal-article","created":{"date-parts":[[2018,10,24]],"date-time":"2018-10-24T11:57:18Z","timestamp":1540382238000},"page":"1-27","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":24,"title":["Safe replication through bounded concurrency verification"],"prefix":"10.1145","volume":"2","author":[{"given":"Gowtham","family":"Kaki","sequence":"first","affiliation":[{"name":"Purdue University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Kapil","family":"Earanky","sequence":"additional","affiliation":[{"name":"Purdue University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"KC","family":"Sivaramakrishnan","sequence":"additional","affiliation":[{"name":"Cambridge University, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Suresh","family":"Jagannathan","sequence":"additional","affiliation":[{"name":"Purdue University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2018,10,24]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_25"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2523616.2523632"},{"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\/2723372.2737784"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2447976.2447992"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2463676.2465279"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.14778\/2212351.2212359"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2741948.2741972"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062353"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009888"},{"key":"e_1_2_2_11_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_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009895"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535848"},{"key":"e_1_2_2_14_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_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2408776.2408795"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/564585.564601"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837625"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535854"},{"key":"e_1_2_2_19_1","volume-title":"https:\/\/jepsen.io\/","author":"Jepsen","year":"2018","unstructured":"Jepsen 2018. ( 2018 ). https:\/\/jepsen.io\/ Jepsen 2018. (2018). https:\/\/jepsen.io\/"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158115"},{"key":"e_1_2_2_21_1","volume-title":"Proceedings of the 4th USENIX Conference on Networked Systems Design &amp;#38; Implementation (NSDI\u201907)","author":"Killian Charles","year":"2007","unstructured":"Charles Killian , James W. Anderson , Ranjit Jhala , and Amin Vahdat . 2007 . Life, Death, and the Critical Transition: Finding Liveness Bugs in Systems Code . In Proceedings of the 4th USENIX Conference on Networked Systems Design &amp;#38; Implementation (NSDI\u201907) . USENIX Association, Berkeley, CA, USA, 18\u201318. http:\/\/dl.acm.org\/citation.cfm?id= 1973430. 1973448 Charles Killian, James W. Anderson, Ranjit Jhala, and Amin Vahdat. 2007. Life, Death, and the Critical Transition: Finding Liveness Bugs in Systems Code. In Proceedings of the 4th USENIX Conference on Networked Systems Design &amp;#38; Implementation (NSDI\u201907). USENIX Association, Berkeley, CA, USA, 18\u201318. http:\/\/dl.acm.org\/citation.cfm?id=1973430. 1973448"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1773912.1773922"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837622"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250785"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.5555\/1855741.1855760"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158114"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3140568"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908118"},{"key":"e_1_2_2_29_1","volume-title":"docs.basho.com\/riak\/kv\/2.2.3\/ Riak NoSQL Database","author":"Riak","year":"2018","unstructured":"Riak 2018. ( 2018 ). docs.basho.com\/riak\/kv\/2.2.3\/ Riak NoSQL Database . Riak 2018. (2018). docs.basho.com\/riak\/kv\/2.2.3\/ Riak NoSQL Database."},{"key":"e_1_2_2_30_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_31_1","unstructured":"M. Shapiro A. Bieniusa N. Pregui\u00e7a V. Balegas and C. Meiklejohn. 2018. Just-Right Consistency: Reconciling Availability and Safety. (Jan. 2018). ArXiv e-prints.  M. Shapiro A. Bieniusa N. Pregui\u00e7a V. Balegas and C. Meiklejohn. 2018. Just-Right Consistency: Reconciling Availability and Safety. (Jan. 2018). ArXiv e-prints."},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.5555\/2050613.2050642"},{"key":"e_1_2_2_33_1","series-title":"Lecture Notes in Computer Science","volume-title":"Stabilization, Safety, and Security of Distributed Systems, Xavier D\u00e9fago, Franck Petit, and Vincent Villain (Eds.)","author":"Shapiro Marc","unstructured":"Marc Shapiro , Nuno Pregui\u00e7a , Carlos Baquero , and Marek Zawirski . 2011b. Conflict-Free Replicated Data Types . In Stabilization, Safety, and Security of Distributed Systems, Xavier D\u00e9fago, Franck Petit, and Vincent Villain (Eds.) . Lecture Notes in Computer Science , Vol. 6976 . Springer Berlin Heidelberg , 386\u2013400. Marc Shapiro, Nuno Pregui\u00e7a, Carlos Baquero, and Marek Zawirski. 2011b. Conflict-Free Replicated Data Types. In Stabilization, Safety, and Security of Distributed Systems, Xavier D\u00e9fago, Franck Petit, and Vincent Villain (Eds.). Lecture Notes in Computer Science, Vol. 6976. Springer Berlin Heidelberg, 386\u2013400."},{"key":"e_1_2_2_34_1","series-title":"Lecture Notes in Computer Science","volume-title":"Stabilization, Safety, and Security of Distributed Systems, Xavier D\u00e9fago, Franck Petit, and Vincent Villain (Eds.)","author":"Shapiro Marc","unstructured":"Marc Shapiro , Nuno Pregui\u00e7a , Carlos Baquero , and Marek Zawirski . 2011c. Conflict-Free Replicated Data Types . In Stabilization, Safety, and Security of Distributed Systems, Xavier D\u00e9fago, Franck Petit, and Vincent Villain (Eds.) . Lecture Notes in Computer Science , Vol. 6976 . Springer Berlin Heidelberg , 386\u2013400. Marc Shapiro, Nuno Pregui\u00e7a, Carlos Baquero, and Marek Zawirski. 2011c. Conflict-Free Replicated Data Types. In Stabilization, Safety, and Security of Distributed Systems, Xavier D\u00e9fago, Franck Petit, and Vincent Villain (Eds.). Lecture Notes in Computer Science, Vol. 6976. Springer Berlin Heidelberg, 386\u2013400."},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737981"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2213836.2213945"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2043556.2043592"},{"key":"e_1_2_2_38_1","volume-title":"Proceedings of the Third International Conference on Parallel and Distributed Information Systems (PDIS \u201994)","author":"Terry Douglas B.","unstructured":"Douglas B. Terry , Alan J. Demers , Karin Petersen , Mike Spreitzer , Marvin Theimer , and Brent W. Welch . 1994. Session Guarantees for Weakly Consistent Replicated Data . In Proceedings of the Third International Conference on Parallel and Distributed Information Systems (PDIS \u201994) . IEEE Computer Society, Washington, DC, USA, 140\u2013149. http:\/\/dl.acm.org\/ citation.cfm?id=645792.668302 Douglas B. Terry, Alan J. Demers, Karin Petersen, Mike Spreitzer, Marvin Theimer, and Brent W. Welch. 1994. Session Guarantees for Weakly Consistent Replicated Data. In Proceedings of the Third International Conference on Parallel and Distributed Information Systems (PDIS \u201994). IEEE Computer Society, Washington, DC, USA, 140\u2013149. http:\/\/dl.acm.org\/ citation.cfm?id=645792.668302"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/224056.224070"},{"key":"e_1_2_2_40_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_41_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_42_1","volume-title":"Consistency in Non-Transactional Distributed Storage Systems. CoRR abs\/1512.00168","author":"Viotti Paolo","year":"2015","unstructured":"Paolo Viotti and Marko Vukolic . 2015. Consistency in Non-Transactional Distributed Storage Systems. CoRR abs\/1512.00168 ( 2015 ). http:\/\/arxiv.org\/abs\/1512.00168 Paolo Viotti and Marko Vukolic. 2015. Consistency in Non-Transactional Distributed Storage Systems. CoRR abs\/1512.00168 (2015). http:\/\/arxiv.org\/abs\/1512.00168"},{"key":"e_1_2_2_43_1","unstructured":"Voldemort 2009. (2009). http:\/\/www.project-voldemort.com\/voldemort\/design.html Voldemort Distributed Database.  Voldemort 2009. (2009). http:\/\/www.project-voldemort.com\/voldemort\/design.html Voldemort Distributed Database."},{"key":"e_1_2_2_44_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\/3276534","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3276534","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3276534","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T19:03:39Z","timestamp":1750273419000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3276534"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,10,24]]},"references-count":44,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2018,10,24]]}},"alternative-id":["10.1145\/3276534"],"URL":"https:\/\/doi.org\/10.1145\/3276534","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,10,24]]},"assertion":[{"value":"2018-10-24","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}