{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T11:32:33Z","timestamp":1770291153316,"version":"3.49.0"},"reference-count":69,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2021,10,15]],"date-time":"2021-10-15T00:00:00Z","timestamp":1634256000000},"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":["2019285, 1763399, 1521523"],"award-info":[{"award-number":["2019285, 1763399, 1521523"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["N66001-21-C-4018"],"award-info":[{"award-number":["N66001-21-C-4018"]}],"id":[{"id":"10.13039\/100000185","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":[[2021,10,20]]},"abstract":"<jats:p>Despite recent advances, guaranteeing the correctness of large-scale distributed applications without compromising performance remains a challenging problem. Network and node failures are inevitable and, for some applications, careful control over how they are handled is essential. Unfortunately, existing approaches either completely hide these failures behind an atomic state machine replication (SMR) interface, or expose all of the network-level details, sacrificing atomicity. We propose a novel, compositional, atomic distributed object (ADO) model for strongly consistent distributed systems that combines the best of both options. The object-oriented API abstracts over protocol-specific details and decouples high-level correctness reasoning from implementation choices. At the same time, it intentionally exposes an abstract view of certain key distributed failure cases, thus allowing for more fine-grained control over them than SMR-like models. We demonstrate that proving properties even of composite distributed systems can be straightforward with our Coq verification framework, Advert, thanks to the ADO model. We also show that a variety of common protocols including multi-Paxos and Chain Replication refine the ADO semantics, which allows one to freely choose among them for an application's implementation without modifying ADO-level correctness proofs.<\/jats:p>","DOI":"10.1145\/3485474","type":"journal-article","created":{"date-parts":[[2021,10,15]],"date-time":"2021-10-15T19:18:28Z","timestamp":1634325508000},"page":"1-31","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":11,"title":["Much ADO about failures: a fault-aware model for compositional verification of strongly consistent distributed systems"],"prefix":"10.1145","volume":"5","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8524-1978","authenticated-orcid":false,"given":"Wolf","family":"Honor\u00e9","sequence":"first","affiliation":[{"name":"Yale University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7581-041X","authenticated-orcid":false,"given":"Jieung","family":"Kim","sequence":"additional","affiliation":[{"name":"Yale University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1595-4849","authenticated-orcid":false,"given":"Ji-Yong","family":"Shin","sequence":"additional","affiliation":[{"name":"Northeastern University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8184-7649","authenticated-orcid":false,"given":"Zhong","family":"Shao","sequence":"additional","affiliation":[{"name":"Yale University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2021,10,15]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-19718-5_1"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535930"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/637437.637447"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/1298455.1298487"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3368454"},{"key":"e_1_2_2_6_1","volume-title":"Proc. of the 13th USENIX Symposium on Operating Systems Design and Implementation (OSDI \u201918)","author":"Chajed Tej","year":"2018","unstructured":"Tej Chajed , Frans Kaashoek , Butler Lampson , and Nickolai Zeldovich . 2018 . Verifying Concurrent Software Using Movers in CSPEC . In Proc. of the 13th USENIX Symposium on Operating Systems Design and Implementation (OSDI \u201918) . USENIX Association, Carlsbad, CA. 306\u2013322. https:\/\/dl.acm.org\/doi\/10.5555\/3291168.3291191 Tej Chajed, Frans Kaashoek, Butler Lampson, and Nickolai Zeldovich. 2018. Verifying Concurrent Software Using Movers in CSPEC. In Proc. of the 13th USENIX Symposium on Operating Systems Design and Implementation (OSDI \u201918). USENIX Association, Carlsbad, CA. 306\u2013322. https:\/\/dl.acm.org\/doi\/10.5555\/3291168.3291191"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1365815.1365816"},{"key":"e_1_2_2_8_1","unstructured":"CorfuDB. 2017. CorfuDB. https:\/\/www.github.com\/CorfuDB\/CorfuDB  CorfuDB. 2017. CorfuDB. https:\/\/www.github.com\/CorfuDB\/CorfuDB"},{"key":"e_1_2_2_9_1","unstructured":"Jeff Dean. 2009. Designs Lessons and Advice from Building Large Distributed Systems. https:\/\/research.cs.cornell.edu\/ladis2009\/talks\/dean-keynote-ladis2009.pdf Keynote from ACM SIGOPS International Workshop on Large Scale Distributed Systems and Middleware  Jeff Dean. 2009. Designs Lessons and Advice from Building Large Distributed Systems. https:\/\/research.cs.cornell.edu\/ladis2009\/talks\/dean-keynote-ladis2009.pdf Keynote from ACM SIGOPS International Workshop on Large Scale Distributed Systems and Middleware"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/WORDS.2001.945126"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_19"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3064176.3064183"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00446-002-0070-8"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2043164.2018477"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1132863.1132867"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676975"},{"key":"e_1_2_2_17_1","volume-title":"Proc. of the 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI \u201916)","author":"Gu Ronghui","year":"2016","unstructured":"Ronghui Gu , Zhong Shao , Hao Chen , Xiongnan Wu , Jieung Kim , Vilhelm Sj\u00f6berg , and David Costanzo . 2016 . CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels . In Proc. of the 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI \u201916) . USENIX Association, Berkeley, CA, USA. 653\u2013669. https:\/\/dl.acm.org\/doi\/10.5555\/3026877.3026928 Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan Wu, Jieung Kim, Vilhelm Sj\u00f6berg, and David Costanzo. 2016. CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels. In Proc. of the 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI \u201916). USENIX Association, Berkeley, CA, USA. 653\u2013669. https:\/\/dl.acm.org\/doi\/10.5555\/3026877.3026928"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3296979.3192381"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1345206.1345233"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2670979.2670986"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815428"},{"key":"e_1_2_2_22_1","volume-title":"Proc. of the 11th USENIX Symposium on Operating Systems Design and Implementation (OSDI \u201914)","author":"Hawblitzel Chris","year":"2014","unstructured":"Chris Hawblitzel , Jon Howell , Jacob R. Lorch , Arjun Narayan , Bryan Parno , Danfeng Zhang , and Brian Zill . 2014 . Ironclad Apps: End-to-end Security via Automated Full-system Verification . In Proc. of the 11th USENIX Symposium on Operating Systems Design and Implementation (OSDI \u201914) . USENIX Association, Berkeley, CA, USA. 165\u2013181. https:\/\/dl.acm.org\/doi\/10.5555\/2685048.2685062 Chris Hawblitzel, Jon Howell, Jacob R. Lorch, Arjun Narayan, Bryan Parno, Danfeng Zhang, and Brian Zill. 2014. Ironclad Apps: End-to-end Security via Automated Full-system Verification. In Proc. of the 11th USENIX Symposium on Operating Systems Design and Implementation (OSDI \u201914). USENIX Association, Berkeley, CA, USA. 165\u2013181. https:\/\/dl.acm.org\/doi\/10.5555\/2685048.2685062"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21668-3_26"},{"key":"e_1_2_2_24_1","doi-asserted-by":"crossref","unstructured":"Wolf Honor\u00e9 Jieung Kim Ji-Yong Shin and Zhong Shao. 2021. Much ADO about Failures: A Fault-Aware Model for Compositional Verification of Strongly Consistent Distributed Systems. Yale Univ.. https:\/\/flint.cs.yale.edu\/publications\/ado.html  Wolf Honor\u00e9 Jieung Kim Ji-Yong Shin and Zhong Shao. 2021. Much ADO about Failures: A Fault-Aware Model for Compositional Verification of Strongly Consistent Distributed Systems. Yale Univ.. https:\/\/flint.cs.yale.edu\/publications\/ado.html","DOI":"10.1145\/3485474"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-53426-7_23"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2948985"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737995"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385980"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-44914-8_13"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/568425.568433"},{"key":"e_1_2_2_31_1","unstructured":"Leslie Lamport. 2005. Generalized Consensus and Paxos. Microsoft.  Leslie Lamport. 2005. Generalized Consensus and Paxos. Microsoft."},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00446-006-0005-x"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1582716.1582783"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/383962.383969"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"e_1_2_2_36_1","unstructured":"Xavier Leroy. 2005\u20132020. The CompCert verified compiler. http:\/\/compcert.inria.fr\/  Xavier Leroy. 2005\u20132020. The CompCert verified compiler. http:\/\/compcert.inria.fr\/"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9155-4"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40184-8_17"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359651"},{"key":"e_1_2_2_40_1","volume-title":"Proc. of the 6th USENIX Symposium on Operating Systems Design and Implementation (OSDI \u201904","volume":"8","author":"MacCormick John","year":"2004","unstructured":"John MacCormick , Nick Murphy , Marc Najork , Chandramohan A. Thekkath , and Lidong Zhou . 2004 . Boxwood: Abstractions as the Foundation for Storage Infrastructure . In Proc. of the 6th USENIX Symposium on Operating Systems Design and Implementation (OSDI \u201904 , Vol. 4). USENIX Association, Berkeley, CA, USA. 8\u2013 8 . https:\/\/dl.acm.org\/doi\/10.5555\/1251254.1251262 John MacCormick, Nick Murphy, Marc Najork, Chandramohan A. Thekkath, and Lidong Zhou. 2004. Boxwood: Abstractions as the Foundation for Storage Infrastructure. In Proc. of the 6th USENIX Symposium on Operating Systems Design and Implementation (OSDI \u201904, Vol. 4). USENIX Association, Berkeley, CA, USA. 8\u20138. https:\/\/dl.acm.org\/doi\/10.5555\/1251254.1251262"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1142\/9789814261456_0001"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3278532.3278566"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/2517349.2517350"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/1189256.1189258"},{"key":"e_1_2_2_45_1","volume-title":"USENIX Annual Technical Conference. USENIX Association","author":"Ongaro Diego","unstructured":"Diego Ongaro and John K. Ousterhout . 2014. In Search of an Understandable Consensus Algorithm . In USENIX Annual Technical Conference. USENIX Association , Berkeley, CA, USA. 305\u2013319. https:\/\/dl.acm.org\/doi\/10.5555\/2643634.2643666 Diego Ongaro and John K. Ousterhout. 2014. In Search of an Understandable Consensus Algorithm. In USENIX Annual Technical Conference. USENIX Association, Berkeley, CA, USA. 305\u2013319. https:\/\/dl.acm.org\/doi\/10.5555\/2643634.2643666"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3140568"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908118"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429100"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/2673577"},{"key":"e_1_2_2_50_1","volume-title":"Proc. of the 6th USENIX Symposium on Operating Systems Design and Implementation (OSDI \u201904","volume":"104","author":"Renesse Robbert Van","unstructured":"Robbert Van Renesse and Fred B. Schneider . 2004. Chain Replication for Supporting High Throughput and Availability . In Proc. of the 6th USENIX Symposium on Operating Systems Design and Implementation (OSDI \u201904 , Vol. 4). USENIX Association, Berkeley, CA, USA. 91\u2013 104 . https:\/\/dl.acm.org\/doi\/10.5555\/1251254.1251261 Robbert Van Renesse and Fred B. Schneider. 2004. Chain Replication for Supporting High Throughput and Availability. In Proc. of the 6th USENIX Symposium on Operating Systems Design and Implementation (OSDI \u201904, Vol. 4). USENIX Association, Berkeley, CA, USA. 91\u2013104. https:\/\/dl.acm.org\/doi\/10.5555\/1251254.1251261"},{"key":"e_1_2_2_51_1","volume-title":"CASPaxos: Replicated State Machines without Logs. CoRR, abs\/1802.07000","author":"Rystsov Denis","year":"2018","unstructured":"Denis Rystsov . 2018. CASPaxos: Replicated State Machines without Logs. CoRR, abs\/1802.07000 ( 2018 ), 15 pages. arXiv:1802.07000. arxiv:1802.07000 Denis Rystsov. 2018. CASPaxos: Replicated State Machines without Logs. CoRR, abs\/1802.07000 (2018), 15 pages. arXiv:1802.07000. arxiv:1802.07000"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454036"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/98163.98167"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158116"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/3357223.3362739"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360562"},{"key":"e_1_2_2_57_1","volume-title":"Tanenbaum and Maarten van Steen","author":"Andrew","year":"2006","unstructured":"Andrew S. Tanenbaum and Maarten van Steen . 2006 . Distributed Systems : Principles and Paradigms (2nd Edition). Prentice-Hall , Inc., Singapore. https:\/\/dl.acm.org\/doi\/10.5555\/1202502 Andrew S. Tanenbaum and Maarten van Steen. 2006. Distributed Systems: Principles and Paradigms (2nd Edition). Prentice-Hall, Inc., Singapore. https:\/\/dl.acm.org\/doi\/10.5555\/1202502"},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192414"},{"key":"e_1_2_2_59_1","volume-title":"Object Storage on CRAQ: High-Throughput Chain Replication for Read-Mostly Workloads. In USENIX Annual Technical Conference. USENIX Association","author":"Terrace Jeff","year":"1855","unstructured":"Jeff Terrace and Michael J. Freedman . 2009 . Object Storage on CRAQ: High-Throughput Chain Replication for Read-Mostly Workloads. In USENIX Annual Technical Conference. USENIX Association , Berkeley, CA, USA. 16 pages. https:\/\/dl.acm.org\/doi\/10.5555\/ 1855 807.1855818 Jeff Terrace and Michael J. Freedman. 2009. Object Storage on CRAQ: High-Throughput Chain Replication for Read-Mostly Workloads. In USENIX Annual Technical Conference. USENIX Association, Berkeley, CA, USA. 16 pages. https:\/\/dl.acm.org\/doi\/10.5555\/1855807.1855818"},{"key":"e_1_2_2_60_1","unstructured":"The AWS Team. 2011. Summary of the Amazon EC2 and Amazon RDS Service Disruption in the US East Region. https:\/\/aws.amazon.com\/message\/65648\/  The AWS Team. 2011. Summary of the Amazon EC2 and Amazon RDS Service Disruption in the US East Region. https:\/\/aws.amazon.com\/message\/65648\/"},{"key":"e_1_2_2_61_1","unstructured":"The Coq Development Team. 1999\u20132018. The Coq Proof Assistant. http:\/\/coq.inria.fr  The Coq Development Team. 1999\u20132018. The Coq Proof Assistant. http:\/\/coq.inria.fr"},{"key":"e_1_2_2_62_1","unstructured":"Ben Treynor. 2011. Today\u2019s Outage for Several Google Services. https:\/\/googleblog.blogspot.com\/2014\/01\/todays-outage-for-several-google.html  Ben Treynor. 2011. Today\u2019s Outage for Several Google Services. https:\/\/googleblog.blogspot.com\/2014\/01\/todays-outage-for-several-google.html"},{"key":"e_1_2_2_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290372"},{"key":"e_1_2_2_64_1","volume-title":"A Note on Distributed Computing","author":"Waldo Jim","unstructured":"Jim Waldo , Geoff Wyant , Ann Wollrath , and Sam Kendall . 1994. A Note on Distributed Computing . IEEE Micro . https:\/\/dl.acm.org\/doi\/10.5555\/974938 Jim Waldo, Geoff Wyant, Ann Wollrath, and Sam Kendall. 1994. A Note on Distributed Computing. IEEE Micro. https:\/\/dl.acm.org\/doi\/10.5555\/974938"},{"key":"e_1_2_2_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314617"},{"key":"e_1_2_2_66_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737958"},{"key":"e_1_2_2_67_1","first-page":"265","article-title":"A Distributed Object Model for the Java","volume":"9","author":"Wollrath Ann","year":"1996","unstructured":"Ann Wollrath , Roger Riggs , and Jim Waldo . 1996 . A Distributed Object Model for the Java System. Comput. Syst. , 9 (1996), 265 \u2013 290 . https:\/\/dl.acm.org\/doi\/10.5555\/1268049.1268066 Ann Wollrath, Roger Riggs, and Jim Waldo. 1996. A Distributed Object Model for the Java System. Comput. Syst., 9 (1996), 265\u2013290. https:\/\/dl.acm.org\/doi\/10.5555\/1268049.1268066","journal-title":"System. Comput. Syst."},{"key":"e_1_2_2_68_1","doi-asserted-by":"publisher","DOI":"10.1145\/2854065.2854081"},{"key":"e_1_2_2_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815404"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3485474","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3485474","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3485474","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:30:15Z","timestamp":1750188615000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3485474"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,10,15]]},"references-count":69,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2021,10,20]]}},"alternative-id":["10.1145\/3485474"],"URL":"https:\/\/doi.org\/10.1145\/3485474","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,10,15]]},"assertion":[{"value":"2021-10-15","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}