{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,13]],"date-time":"2025-11-13T18:25:35Z","timestamp":1763058335911,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":60,"publisher":"ACM","license":[{"start":{"date-parts":[[2019,11,20]],"date-time":"2019-11-20T00:00:00Z","timestamp":1574208000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF-1637385, CCF-1521523, CCF-1763399, CNS-1715154"],"award-info":[{"award-number":["CCF-1637385, CCF-1521523, CCF-1763399, CNS-1715154"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2019,11,20]]},"DOI":"10.1145\/3357223.3362739","type":"proceedings-article","created":{"date-parts":[[2019,11,11]],"date-time":"2019-11-11T18:15:00Z","timestamp":1573496100000},"page":"299-311","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":10,"title":["WormSpace"],"prefix":"10.1145","author":[{"given":"Ji-Yong","family":"Shin","sequence":"first","affiliation":[{"name":"Yale University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jieung","family":"Kim","sequence":"additional","affiliation":[{"name":"Yale University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wolf","family":"Honor\u00e9","sequence":"additional","affiliation":[{"name":"Yale University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hern\u00e1n","family":"Vanzetto","sequence":"additional","affiliation":[{"name":"Yale University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Srihari","family":"Radhakrishnan","sequence":"additional","affiliation":[{"name":"Duke University and Yale University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mahesh","family":"Balakrishnan","sequence":"additional","affiliation":[{"name":"Facebook, Inc. and Yale University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhong","family":"Shao","sequence":"additional","affiliation":[{"name":"Yale University"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2019,11,20]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1987.233145"},{"volume-title":"USENIX Conference on Hot Topics in Operating Systems. 20--20","author":"Alagappan Ramnatthan","key":"e_1_3_2_1_2_1","unstructured":"Ramnatthan Alagappan , Vijay Chidambaram , Thanumalayan Sankaranarayana Pillai , Aws Albarghouthi , Andrea C. Arpac-Dusseau , and Remzi H . Arpaci-Dusseau. 2015. Beyond storage APIs: provable semantics for storage stacks . In USENIX Conference on Hot Topics in Operating Systems. 20--20 . Ramnatthan Alagappan, Vijay Chidambaram, Thanumalayan Sankaranarayana Pillai, Aws Albarghouthi, Andrea C. Arpac-Dusseau, and Remzi H. Arpaci-Dusseau. 2015. Beyond storage APIs: provable semantics for storage stacks. In USENIX Conference on Hot Topics in Operating Systems. 20--20."},{"key":"e_1_3_2_1_3_1","volume-title":"USENIX Symposium on Networked Systems Design and Implementation. 1--14","author":"Balakrishnan Mahesh","year":"2012","unstructured":"Mahesh Balakrishnan , Dahlia Malkhi , Vijayan Prabhakaran , Ted Wobber , Michael Wei , and John D Davis . 2012 . CORFU: a shared log design for flash clusters .. In USENIX Symposium on Networked Systems Design and Implementation. 1--14 . Mahesh Balakrishnan, Dahlia Malkhi, Vijayan Prabhakaran, Ted Wobber, Michael Wei, and John D Davis. 2012. CORFU: a shared log design for flash clusters.. In USENIX Symposium on Networked Systems Design and Implementation. 1--14."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2517349.2522732"},{"key":"e_1_3_2_1_5_1","volume-title":"Biennial Conference on Innovative Data Systems Research. 9--12","author":"Bernstein Philip A","year":"2011","unstructured":"Philip A Bernstein , Colin W Reid , and Sudipto Das . 2011 . Hyder - a transactional record manager for shared flash . In Biennial Conference on Innovative Data Systems Research. 9--12 . Philip A Bernstein, Colin W Reid, and Sudipto Das. 2011. Hyder - a transactional record manager for shared flash. In Biennial Conference on Innovative Data Systems Research. 9--12."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/163298.163303"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/637437.637447"},{"key":"e_1_3_2_1_8_1","volume-title":"USENIX Security Symposium. 917--934","author":"Bond Barry","year":"2017","unstructured":"Barry Bond , Chris Hawblitzel , Manos Kapritsos , K. Rustan M. Leino , Jacob R. Lorch , Bryan Parno , Ashay Rane , Srinath T. V. Setty , and Laure Thompson . 2017 . Vale: verifying high-performance cryptographic assembly code . In USENIX Security Symposium. 917--934 . Barry Bond, Chris Hawblitzel, Manos Kapritsos, K. Rustan M. Leino, Jacob R. Lorch, Bryan Parno, Ashay Rane, Srinath T. V. Setty, and Laure Thompson. 2017. Vale: verifying high-performance cryptographic assembly code. In USENIX Security Symposium. 917--934."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/1267308.1267332"},{"key":"e_1_3_2_1_10_1","volume-title":"USENIX Symposium on Operating Systems Design and Implementation. 173--186","author":"Castro Miguel","year":"1999","unstructured":"Miguel Castro and Barbara Liskov . 1999 . Practical Byzantine fault tolerance . In USENIX Symposium on Operating Systems Design and Implementation. 173--186 . Miguel Castro and Barbara Liskov. 1999. Practical Byzantine fault tolerance. In USENIX Symposium on Operating Systems Design and Implementation. 173--186."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815402"},{"key":"e_1_3_2_1_12_1","volume-title":"USENIX Symposium on Operating Systems Design and Implementation. 177--190","author":"Cowling James","year":"2006","unstructured":"James Cowling , Daniel Myers , Barbara Liskov , Rodrigo Rodrigues , and Liuba Shrira . 2006 . HQ replication: a hybrid quorum protocol for Byzantine fault tolerance . In USENIX Symposium on Operating Systems Design and Implementation. 177--190 . James Cowling, Daniel Myers, Barbara Liskov, Rodrigo Rodrigues, and Liuba Shrira. 2006. HQ replication: a hybrid quorum protocol for Byzantine fault tolerance. In USENIX Symposium on Operating Systems Design and Implementation. 177--190."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_3_2_1_14_1","unstructured":"The Coq development team. 2018. The Coq proof assistant. http:\/\/coq.inria.fr.  The Coq development team. 2018. The Coq proof assistant. http:\/\/coq.inria.fr."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132782"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3064176.3064183"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/71.910869"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00446-002-0070-8"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89884-1_32"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1132863.1132867"},{"volume-title":"Operating Systems: An Advanced Course","author":"Gray James N","key":"e_1_3_2_1_22_1","unstructured":"James N Gray . 1978. Notes on data base operating systems . In Operating Systems: An Advanced Course . Springer , 393--481. James N Gray. 1978. Notes on data base operating systems. In Operating Systems: An Advanced Course. Springer, 393--481."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676975"},{"key":"e_1_3_2_1_24_1","volume-title":"USENIX Conference on Operating Systems Design and Implementation. 653--669","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 USENIX Conference on Operating Systems Design and Implementation. 653--669 . 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 USENIX Conference on Operating Systems Design and Implementation. 653--669."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192381"},{"volume-title":"Fault-Tolerant Distributed Computing","author":"Hadzilacos Vassos","key":"e_1_3_2_1_26_1","unstructured":"Vassos Hadzilacos . 1990. On the relationship between the atomic commitment and consensus problems . In Fault-Tolerant Distributed Computing . Springer , 201--208. Vassos Hadzilacos. 1990. On the relationship between the atomic commitment and consensus problems. In Fault-Tolerant Distributed Computing. Springer, 201--208."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815428"},{"key":"e_1_3_2_1_28_1","volume-title":"USENIX Conference on Operating Systems Design and Implementation. 165--181","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 USENIX Conference on Operating Systems Design and Implementation. 165--181 . 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 USENIX Conference on Operating Systems Design and Implementation. 165--181."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/114005.102808"},{"key":"e_1_3_2_1_30_1","volume-title":"USENIX Annual Technical Conference","volume":"8","author":"Hunt Patrick","year":"2010","unstructured":"Patrick Hunt , Mahadev Konar , Flavio Paiva Junqueira , and Benjamin Reed . 2010 . ZooKeeper: wait-free coordination for internet-scale systems . In USENIX Annual Technical Conference , Vol. 8 . 9. Patrick Hunt, Mahadev Konar, Flavio Paiva Junqueira, and Benjamin Reed. 2010. ZooKeeper: wait-free coordination for internet-scale systems. In USENIX Annual Technical Conference, Vol. 8. 9."},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/DSN.2011.5958223"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-71237-6_14"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/279227.279229"},{"key":"e_1_3_2_1_34_1","first-page":"4","article-title":"Paxos made simple","volume":"32","author":"Lamport Leslie","year":"2001","unstructured":"Leslie Lamport . 2001 . Paxos made simple . SIGACT News 32 , 4 (Dec. 2001), 51--58. Leslie Lamport. 2001. Paxos made simple. SIGACT News 32, 4 (Dec. 2001), 51--58.","journal-title":"SIGACT News"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1582716.1582783"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/SRDS.2007.32"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103711"},{"key":"e_1_3_2_1_39_1","volume-title":"ACM Symposium on Operating Systems Principles. 80--92","author":"Liu Xiaoming","year":"1999","unstructured":"Xiaoming Liu , Christoph Kreitz , Robbert Van Renesse , Jason Hickey , Mark Hay-den, Kenneth Birman , and Robert Constable . 1999 . Building reliable, highperformance communication systems from components . In ACM Symposium on Operating Systems Principles. 80--92 . Xiaoming Liu, Christoph Kreitz, Robbert Van Renesse, Jason Hickey, Mark Hay-den, Kenneth Birman, and Robert Constable. 1999. Building reliable, highperformance communication systems from components. In ACM Symposium on Operating Systems Principles. 80--92."},{"key":"e_1_3_2_1_40_1","volume-title":"USENIX Symposium on Operating Systems Design and Implementation. 357--372","author":"Lockerman Joshua","year":"2018","unstructured":"Joshua Lockerman , Jose M Faleiro , Juno Kim , Soham Sankaran , Daniel J Abadi , James Aspnes , Siddhartha Sen , and Mahesh Balakrishnan . 2018 . The FuzzyLog: a partially ordered shared log . In USENIX Symposium on Operating Systems Design and Implementation. 357--372 . Joshua Lockerman, Jose M Faleiro, Juno Kim, Soham Sankaran, Daniel J Abadi, James Aspnes, Siddhartha Sen, and Mahesh Balakrishnan. 2018. The FuzzyLog: a partially ordered shared log. In USENIX Symposium on Operating Systems Design and Implementation. 357--372."},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2451116.2451148"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/2146382.2146391"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/2517349.2517350"},{"key":"e_1_3_2_1_44_1","volume-title":"USENIX Conference on Operating Systems Design and Implementation. 517--532","author":"Mu Shuai","year":"2016","unstructured":"Shuai Mu , Lamont Nelson , Wyatt Lloyd , and Jinyang Li . 2016 . Consolidating concurrency control and consensus for commits under conflicts . In USENIX Conference on Operating Systems Design and Implementation. 517--532 . Shuai Mu, Lamont Nelson, Wyatt Lloyd, and Jinyang Li. 2016. Consolidating concurrency control and consensus for commits under conflicts. In USENIX Conference on Operating Systems Design and Implementation. 517--532."},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132748"},{"key":"e_1_3_2_1_46_1","volume-title":"USENIX Annual Technical Conference. 305--319","author":"Ongaro Diego","year":"2014","unstructured":"Diego Ongaro and John K Ousterhout . 2014 . In search of an understandable consensus algorithm . In USENIX Annual Technical Conference. 305--319 . Diego Ongaro and John K Ousterhout. 2014. In search of an understandable consensus algorithm. In USENIX Annual Technical Conference. 305--319."},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3140568"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/72981.72992"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/98163.98167"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158116"},{"key":"e_1_3_2_1_51_1","volume-title":"USENIX Conference on Operating Systems Design and Implementation. 1--16","author":"Sigurbjarnarson Helgi","year":"2016","unstructured":"Helgi Sigurbjarnarson , James Bornholt , Emina Torlak , and Xi Wang . 2016 . Pushbutton verification of file systems via crash refinement . In USENIX Conference on Operating Systems Design and Implementation. 1--16 . Helgi Sigurbjarnarson, James Bornholt, Emina Torlak, and Xi Wang. 2016. Pushbutton verification of file systems via crash refinement. In USENIX Conference on Operating Systems Design and Implementation. 1--16."},{"key":"e_1_3_2_1_52_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 ( 2 nd edition). Prentice-Hall , Inc. Andrew S. Tanenbaum and Maarten van Steen. 2006. Distributed systems: principles and paradigms (2nd edition). Prentice-Hall, Inc.","edition":"2"},{"key":"e_1_3_2_1_53_1","volume-title":"ACM SIGPLAN Conference on Programming Language Design and Implementation. 662--677","author":"Taube Marcelo","year":"2018","unstructured":"Marcelo Taube , Giuliano Losa , Kenneth L. McMillan , Oded Padon , Mooly Sagiv , Sharon Shoham , James R. Wilcox , and Doug Woos . 2018 . Modularity for decidability: implementing and semi-automatically verifying distributed systems . In ACM SIGPLAN Conference on Programming Language Design and Implementation. 662--677 . Marcelo Taube, Giuliano Losa, Kenneth L. McMillan, Oded Padon, Mooly Sagiv, Sharon Shoham, James R. Wilcox, and Doug Woos. 2018. Modularity for decidability: implementing and semi-automatically verifying distributed systems. In ACM SIGPLAN Conference on Programming Language Design and Implementation. 662--677."},{"key":"e_1_3_2_1_54_1","volume-title":"USENIX Annual Technical Conference. 11--11","author":"Terrace Jeff","year":"2009","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. 11--11 . Jeff Terrace and Michael J Freedman. 2009. Object storage on CRAQ: high-throughput chain replication for read-mostly workloads. In USENIX Annual Technical Conference. 11--11."},{"key":"e_1_3_2_1_55_1","first-page":"42","article-title":"Paxos made moderately complex","volume":"47","author":"Renesse Robbert Van","year":"2015","unstructured":"Robbert Van Renesse and Deniz Altinbuken . 2015 . Paxos made moderately complex . Comput. Surveys 47 , 3 (2015), 42 . Robbert Van Renesse and Deniz Altinbuken. 2015. Paxos made moderately complex. Comput. Surveys 47, 3 (2015), 42.","journal-title":"Comput. Surveys"},{"key":"e_1_3_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/227210.227229"},{"key":"e_1_3_2_1_57_1","volume-title":"USENIX Conference on Operating Systems Design and Implementation. 91--104","author":"Renesse Robbert Van","year":"2004","unstructured":"Robbert Van Renesse and Fred B Schneider . 2004 . Chain replication for supporting high throughput and availability .. In USENIX Conference on Operating Systems Design and Implementation. 91--104 . Robbert Van Renesse and Fred B Schneider. 2004. Chain replication for supporting high throughput and availability.. In USENIX Conference on Operating Systems Design and Implementation. 91--104."},{"key":"e_1_3_2_1_58_1","unstructured":"VMware Research. 2018. CorfuDB. https:\/\/www.github.com\/CorfuDB\/CorfuDB.  VMware Research. 2018. CorfuDB. https:\/\/www.github.com\/CorfuDB\/CorfuDB."},{"key":"e_1_3_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737958"},{"key":"e_1_3_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/2854065.2854081"},{"volume-title":"ACM Symposium on Operating Systems Principles. 263--278","author":"Zhang Irene","key":"e_1_3_2_1_61_1","unstructured":"Irene Zhang , Naveen Kr. Sharma , Adriana Szekeres , Arvind Krishnamurthy , and Dan R. K. Ports . 2015. Building consistent transactions with inconsistent replication . In ACM Symposium on Operating Systems Principles. 263--278 . Irene Zhang, Naveen Kr. Sharma, Adriana Szekeres, Arvind Krishnamurthy, and Dan R. K. Ports. 2015. Building consistent transactions with inconsistent replication. In ACM Symposium on Operating Systems Principles. 263--278."}],"event":{"name":"SoCC '19: ACM Symposium on Cloud Computing","sponsor":["SIGMOD ACM Special Interest Group on Management of Data","SIGOPS ACM Special Interest Group on Operating Systems"],"location":"Santa Cruz CA USA","acronym":"SoCC '19"},"container-title":["Proceedings of the ACM Symposium on Cloud Computing"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3357223.3362739","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3357223.3362739","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3357223.3362739","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:13:44Z","timestamp":1750202024000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3357223.3362739"}},"subtitle":["A Modular Foundation for Simple, Verifiable Distributed Systems"],"short-title":[],"issued":{"date-parts":[[2019,11,20]]},"references-count":60,"alternative-id":["10.1145\/3357223.3362739","10.1145\/3357223"],"URL":"https:\/\/doi.org\/10.1145\/3357223.3362739","relation":{},"subject":[],"published":{"date-parts":[[2019,11,20]]},"assertion":[{"value":"2019-11-20","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}