{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,28]],"date-time":"2026-02-28T17:32:41Z","timestamp":1772299961519,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":54,"publisher":"ACM","license":[{"start":{"date-parts":[[2021,10,26]],"date-time":"2021-10-26T00:00:00Z","timestamp":1635206400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc-nd\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2021,10,26]]},"DOI":"10.1145\/3477132.3483540","type":"proceedings-article","created":{"date-parts":[[2021,10,19]],"date-time":"2021-10-19T15:59:18Z","timestamp":1634659158000},"page":"836-850","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":57,"title":["Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3"],"prefix":"10.1145","author":[{"given":"James","family":"Bornholt","sequence":"first","affiliation":[{"name":"Amazon Web Services & The University of Texas at Austin"}]},{"given":"Rajeev","family":"Joshi","sequence":"additional","affiliation":[{"name":"Amazon Web Services"}]},{"given":"Vytautas","family":"Astrauskas","sequence":"additional","affiliation":[{"name":"ETH Zurich"}]},{"given":"Brendan","family":"Cully","sequence":"additional","affiliation":[{"name":"Amazon Web Services"}]},{"given":"Bernhard","family":"Kragl","sequence":"additional","affiliation":[{"name":"Amazon Web Services"}]},{"given":"Seth","family":"Markle","sequence":"additional","affiliation":[{"name":"Amazon Web Services"}]},{"given":"Kyle","family":"Sauri","sequence":"additional","affiliation":[{"name":"Amazon Web Services"}]},{"given":"Drew","family":"Schleit","sequence":"additional","affiliation":[{"name":"Amazon Web Services"}]},{"given":"Grant","family":"Slatton","sequence":"additional","affiliation":[{"name":"Amazon Web Services"}]},{"given":"Serdar","family":"Tasiran","sequence":"additional","affiliation":[{"name":"Amazon Web Services"}]},{"given":"Jacob","family":"Van Geffen","sequence":"additional","affiliation":[{"name":"University of Washington"}]},{"given":"Andrew","family":"Warfield","sequence":"additional","affiliation":[{"name":"Amazon Web Services"}]}],"member":"320","published-online":{"date-parts":[[2021,10,26]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Proc. ACM Program. Lang. 4, OOPSLA","author":"Astrauskas Vytautas","year":"2020","unstructured":"Vytautas Astrauskas , Christoph Matheja , Federico Poli , Peter M\u00fcller , and Alexander J. Summers . 2020. How do programmers use unsafe Rust? Proc. ACM Program. Lang. 4, OOPSLA ( 2020 ), 136:1--136:27. Vytautas Astrauskas, Christoph Matheja, Federico Poli, Peter M\u00fcller, and Alexander J. Summers. 2020. How do programmers use unsafe Rust? Proc. ACM Program. Lang. 4, OOPSLA (2020), 136:1--136:27."},{"key":"e_1_3_2_1_2_1","volume-title":"Proc. ACM Program. Lang. 3, OOPSLA","author":"Astrauskas Vytautas","year":"2019","unstructured":"Vytautas Astrauskas , Peter M\u00fcller , Federico Poli , and Alexander J. Summers . 2019. Leveraging Rust types for modular specification and verification . Proc. ACM Program. Lang. 3, OOPSLA ( 2019 ), 147:1--147:30. Vytautas Astrauskas, Peter M\u00fcller, Federico Poli, and Alexander J. Summers. 2019. Leveraging Rust types for modular specification and verification. Proc. ACM Program. Lang. 3, OOPSLA (2019), 147:1--147:30."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-01090-4_32"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2872362.2872406"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1736020.1736040"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359632"},{"key":"e_1_3_2_1_7_1","volume-title":"Proceedings of the 15th Symposium on Operating Systems Design and Implementation (OSDI). Virtual, 423--439","author":"Chajed Tej","year":"2021","unstructured":"Tej Chajed , Joseph Tassarotti , Mark Theng , Ralf Jung , M. Frans Kaashoek , and Nickolai Zeldovich . 2021 . GoJournal: a verified, concurrent, crash-safe journaling system . In Proceedings of the 15th Symposium on Operating Systems Design and Implementation (OSDI). Virtual, 423--439 . Tej Chajed, Joseph Tassarotti, Mark Theng, Ralf Jung, M. Frans Kaashoek, and Nickolai Zeldovich. 2021. GoJournal: a verified, concurrent, crash-safe journaling system. In Proceedings of the 15th Symposium on Operating Systems Design and Implementation (OSDI). Virtual, 423--439."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815402"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/351240.351266"},{"key":"e_1_3_2_1_10_1","volume-title":"Proceedings of the 28th ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA)","author":"Coons Katherine E.","unstructured":"Katherine E. Coons , Madan Musuvathi , and Kathryn S . McKinley. 2013. Bounded partial-order reduction . In Proceedings of the 28th ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA) . Indianapolis, IN, USA, 833--848. Katherine E. Coons, Madan Musuvathi, and Kathryn S. McKinley. 2013. Bounded partial-order reduction. In Proceedings of the 28th ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA). Indianapolis, IN, USA, 833--848."},{"key":"e_1_3_2_1_11_1","unstructured":"Ankush Desai. 2021. P. https:\/\/github.com\/p-org\/p  Ankush Desai. 2021. P. https:\/\/github.com\/p-org\/p"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462184"},{"key":"e_1_3_2_1_13_1","volume-title":"Proc. ACM Program. Lang. 2, OOPSLA","author":"Desai Ankush","year":"2018","unstructured":"Ankush Desai , Amar Phanishayee , Shaz Qadeer , and Sanjit A. Seshia . 2018. Compositional programming and testing of dynamic distributed systems . Proc. ACM Program. Lang. 2, OOPSLA ( 2018 ), 159:1--159:30. Ankush Desai, Amar Phanishayee, Shaz Qadeer, and Sanjit A. Seshia. 2018. Compositional programming and testing of dynamic distributed systems. Proc. ACM Program. Lang. 2, OOPSLA (2018), 159:1--159:30."},{"key":"e_1_3_2_1_14_1","unstructured":"Craig Disselkoen Sunjay Cauligi Dean Tullsen and Deian Stefan. 2020. Finding and Eliminating Timing Side-Channels in Crypto Code with Pitchfork. In TECHCON.  Craig Disselkoen Sunjay Cauligi Dean Tullsen and Deian Stefan. 2020. Finding and Eliminating Timing Side-Channels in Crypto Code with Pitchfork. In TECHCON."},{"key":"e_1_3_2_1_15_1","unstructured":"Facebook. 2021. MIRAI. https:\/\/github.com\/facebookexperimental\/MIRAI  Facebook. 2021. MIRAI. https:\/\/github.com\/facebookexperimental\/MIRAI"},{"key":"e_1_3_2_1_16_1","volume-title":"Proceedings of the 1st Symposium on Operating Systems Design and Implementation (OSDI)","author":"Gregory","unstructured":"Gregory R. Ganger and Yale N. Patt. 1994. Metadata Update Performance in File Systems . In Proceedings of the 1st Symposium on Operating Systems Design and Implementation (OSDI) . Monterey, CA, USA, 49--60. Gregory R. Ganger and Yale N. Patt. 1994. Metadata Update Performance in File Systems. In Proceedings of the 1st Symposium on Operating Systems Design and Implementation (OSDI). Monterey, CA, USA, 49--60."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263717"},{"key":"e_1_3_2_1_18_1","volume-title":"Proceedings of the 14th Symposium on Operating Systems Design and Implementation (OSDI). Virtual Event, 99--115","author":"Hance Travis","year":"2020","unstructured":"Travis Hance , Andrea Lattuada , Chris Hawblitzel , Jon Howell , Rob Johnson , and Bryan Parno . 2020 . Storage Systems are Distributed Systems (So Verify Them ThatWay!) . In Proceedings of the 14th Symposium on Operating Systems Design and Implementation (OSDI). Virtual Event, 99--115 . Travis Hance, Andrea Lattuada, Chris Hawblitzel, Jon Howell, Rob Johnson, and Bryan Parno. 2020. Storage Systems are Distributed Systems (So Verify Them ThatWay!). In Proceedings of the 14th Symposium on Operating Systems Design and Implementation (OSDI). Virtual Event, 99--115."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/78969.78972"},{"key":"e_1_3_2_1_20_1","volume-title":"Proceedings of the International Symposium on Software Testing and Analysis (ISSTA)","author":"Hildebrandt Ralf","year":"2000","unstructured":"Ralf Hildebrandt and Andreas Zeller . 2000 . Simplifying failureinducing input . In Proceedings of the International Symposium on Software Testing and Analysis (ISSTA) . Portland, OR, USA, 135--145. Ralf Hildebrandt and Andreas Zeller. 2000. Simplifying failureinducing input. In Proceedings of the International Symposium on Software Testing and Analysis (ISSTA). Portland, OR, USA, 135--145."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_64"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"key":"e_1_3_2_1_23_1","volume-title":"Software Abstractions: logic, language, and analysis","author":"Jackson Daniel","unstructured":"Daniel Jackson . 2009. Software Abstractions: logic, language, and analysis ( 2 nd ed.). MIT Press . Daniel Jackson. 2009. Software Abstractions: logic, language, and analysis (2nd ed.). MIT Press.","edition":"2"},{"key":"e_1_3_2_1_24_1","volume-title":"Lightweight Formal Methods. Computer 29, 4","author":"Jackson Daniel","year":"1996","unstructured":"Daniel Jackson and Jeannette Wing . 1996. Lightweight Formal Methods. Computer 29, 4 ( 1996 ). Daniel Jackson and Jeannette Wing. 1996. Lightweight Formal Methods. Computer 29, 4 (1996)."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-006-0022-3"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87603-8_23"},{"key":"e_1_3_2_1_27_1","volume-title":"Usable Auto-Active Verification. In Workshop on Usable Verification","author":"K. Rustan","unstructured":"K. Rustan M. Leino and Micha\u0142 Moskal. 2010 . Usable Auto-Active Verification. In Workshop on Usable Verification . Redmond, WA, USA. K. Rustan M. Leino and Micha\u0142 Moskal. 2010. Usable Auto-Active Verification. In Workshop on Usable Verification. Redmond, WA, USA."},{"key":"e_1_3_2_1_28_1","unstructured":"Carl Lerche. 2020. Loom. https:\/\/github.com\/tokio-rs\/loom  Carl Lerche. 2020. Loom. https:\/\/github.com\/tokio-rs\/loom"},{"key":"e_1_3_2_1_29_1","volume-title":"Automating safe, hands-off deployments","author":"Ligouri Clare","unstructured":"Clare Ligouri . 2020. Automating safe, hands-off deployments . Amazon Builders' Library . https:\/\/aws.amazon.com\/builders-library\/automating-safe-hands-off-deployments\/ Clare Ligouri. 2020. Automating safe, hands-off deployments. Amazon Builders' Library. https:\/\/aws.amazon.com\/builders-library\/automating-safe-hands-off-deployments\/"},{"key":"e_1_3_2_1_30_1","unstructured":"Jason Lingle. 2020. Proptest. https:\/\/github.com\/AltSysrq\/proptest  Jason Lingle. 2020. Proptest. https:\/\/github.com\/AltSysrq\/proptest"},{"key":"e_1_3_2_1_31_1","volume-title":"Proceedings of the 14th USENIX Conference on File and Storage Technologies (FAST)","author":"Lu Lanyue","unstructured":"Lanyue Lu , Thanumalayan Sankaranarayana Pillai , Andrea C. Arpaci-Dusseau , and Remzi H . Arpaci-Dusseau. 2016. WiscKey: Separating Keys from Values in SSD-conscious Storage . In Proceedings of the 14th USENIX Conference on File and Storage Technologies (FAST) . Santa Clara, CA, USA, 133--148. Lanyue Lu, Thanumalayan Sankaranarayana Pillai, Andrea C. Arpaci-Dusseau, and Remzi H. Arpaci-Dusseau. 2016. WiscKey: Separating Keys from Values in SSD-conscious Storage. In Proceedings of the 14th USENIX Conference on File and Storage Technologies (FAST). Santa Clara, CA, USA, 133--148."},{"key":"e_1_3_2_1_32_1","first-page":"1","article-title":"Test-Case Reduction via Test-Case Generation: Insights from the Hypothesis Reducer. In Proceedings of the 34th European Conference on Object-Oriented Programming (ECOOP). Berlin","volume":"13","author":"Maciver David","year":"2020","unstructured":"David Maciver and Alastair F. Donaldson . 2020 . Test-Case Reduction via Test-Case Generation: Insights from the Hypothesis Reducer. In Proceedings of the 34th European Conference on Object-Oriented Programming (ECOOP). Berlin , Germany , 13 : 1 -- 13 :27. David Maciver and Alastair F. Donaldson. 2020. Test-Case Reduction via Test-Case Generation: Insights from the Hypothesis Reducer. In Proceedings of the 34th European Conference on Object-Oriented Programming (ECOOP). Berlin, Germany, 13:1--13:27.","journal-title":"Germany"},{"key":"e_1_3_2_1_33_1","volume-title":"Proceedings of the 13th Symposium on Operating Systems Design and Implementation (OSDI)","author":"Mohan Jayashree","year":"2018","unstructured":"Jayashree Mohan , Ashlie Martinez , Soujanya Ponnapalli , Pandian Raju , and Vijay Chidambaram . 2018 . Finding Crash-Consistency Bugs with Bounded Black-Box Crash Testing . In Proceedings of the 13th Symposium on Operating Systems Design and Implementation (OSDI) . Carlsbad, CA, USA, 33--50. Jayashree Mohan, Ashlie Martinez, Soujanya Ponnapalli, Pandian Raju, and Vijay Chidambaram. 2018. Finding Crash-Consistency Bugs with Bounded Black-Box Crash Testing. In Proceedings of the 13th Symposium on Operating Systems Design and Implementation (OSDI). Carlsbad, CA, USA, 33--50."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628143"},{"key":"e_1_3_2_1_35_1","volume-title":"Proceedings of the 8th Symposium on Operating Systems Design and Implementation (OSDI)","author":"Musuvathi Madanlal","year":"2008","unstructured":"Madanlal Musuvathi , Shaz Qadeer , Thomas Ball , G\u00e9rard Basler , Piramanayagam Arumuga Nainar , and Iulian Neamtiu . 2008 . Finding and Reproducing Heisenbugs in Concurrent Programs . In Proceedings of the 8th Symposium on Operating Systems Design and Implementation (OSDI) . San Diego, CA, USA, 267--280. Madanlal Musuvathi, Shaz Qadeer, Thomas Ball, G\u00e9rard Basler, Piramanayagam Arumuga Nainar, and Iulian Neamtiu. 2008. Finding and Reproducing Heisenbugs in Concurrent Programs. In Proceedings of the 8th Symposium on Operating Systems Design and Implementation (OSDI). San Diego, CA, USA, 267--280."},{"key":"e_1_3_2_1_36_1","unstructured":"Vishwas Narendra Serdar Tasiran and Ankush Desai. 2021. Amazon S3 Strong Consistency. https:\/\/www.youtube.com\/watch?v=B0yXz6EeCaA  Vishwas Narendra Serdar Tasiran and Ankush Desai. 2021. Amazon S3 Strong Consistency. https:\/\/www.youtube.com\/watch?v=B0yXz6EeCaA"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132748"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2699417"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509514"},{"key":"e_1_3_2_1_40_1","unstructured":"Project Oak. 2021. Rust Verification Tools. https:\/\/github.com\/projectoak\/rust-verification-tools\/  Project Oak. 2021. Rust Verification Tools. https:\/\/github.com\/projectoak\/rust-verification-tools\/"},{"key":"e_1_3_2_1_41_1","first-page":"4","article-title":"The Log-Structured Merge-Tree (LSM-Tree)","volume":"33","author":"O'Neil Patrick","year":"1996","unstructured":"Patrick O'Neil , Edward Cheng , Dieter Gawlick , and Elizabeth O'Neil . 1996 . The Log-Structured Merge-Tree (LSM-Tree) . Acta Informatica 33 , 4 (June 1996), 351--385. Patrick O'Neil, Edward Cheng, Dieter Gawlick, and Elizabeth O'Neil. 1996. The Log-Structured Merge-Tree (LSM-Tree). Acta Informatica 33, 4 (June 1996), 351--385.","journal-title":"Acta Informatica"},{"key":"e_1_3_2_1_42_1","volume-title":"Proceedings of the 11th Symposium on Operating Systems Design and Implementation (OSDI)","author":"Pillai Thanumalayan Sankaranarayana","unstructured":"Thanumalayan Sankaranarayana Pillai , Vijay Chidambaram , Ramnatthan Alagappan , Samer Al-Kiswany , Andrea C. Arpaci-Dusseau , and Remzi H . Arpaci-Dusseau. 2014. All File Systems Are Not Created Equal: On the Complexity of Crafting Crash-Consistent Applications . In Proceedings of the 11th Symposium on Operating Systems Design and Implementation (OSDI) . Broomfield, CO, USA, 433--448. Thanumalayan Sankaranarayana Pillai, Vijay Chidambaram, Ramnatthan Alagappan, Samer Al-Kiswany, Andrea C. Arpaci-Dusseau, and Remzi H. Arpaci-Dusseau. 2014. All File Systems Are Not Created Equal: On the Complexity of Crafting Crash-Consistent Applications. In Proceedings of the 11th Symposium on Operating Systems Design and Implementation (OSDI). Broomfield, CO, USA, 433--448."},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.5555\/1267903.1267905"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254104"},{"key":"e_1_3_2_1_45_1","unstructured":"Alastair Reid and Shaked Flur. 2021. Rust Verification Tools: Retrospective. https:\/\/project-oak.github.io\/rust-verification-tools\/2021\/09\/01\/retrospective.html  Alastair Reid and Shaked Flur. 2021. Rust Verification Tools: Retrospective. https:\/\/project-oak.github.io\/rust-verification-tools\/2021\/09\/01\/retrospective.html"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815411"},{"key":"e_1_3_2_1_47_1","unstructured":"Amazon Web Services. 2020. Shuttle. https:\/\/github.com\/awslabs\/shuttle  Amazon Web Services. 2020. Shuttle. https:\/\/github.com\/awslabs\/shuttle"},{"key":"e_1_3_2_1_48_1","unstructured":"Amazon Web Services. 2021. Rust Model Checker (RMC). https:\/\/github.com\/model-checking\/rmc  Amazon Web Services. 2021. Rust Model Checker (RMC). https:\/\/github.com\/model-checking\/rmc"},{"key":"e_1_3_2_1_49_1","volume-title":"Proceedings of the 12th Symposium on Operating Systems Design and Implementation (OSDI)","author":"Sigurbjarnarson Helgi","year":"2016","unstructured":"Helgi Sigurbjarnarson , James Bornholt , Emina Torlak , and Xi Wang . 2016 . Push-Button Verification of File Systems via Crash Refinement . In Proceedings of the 12th Symposium on Operating Systems Design and Implementation (OSDI) . Savannah, GA, USA, 1--16. Helgi Sigurbjarnarson, James Bornholt, Emina Torlak, and Xi Wang. 2016. Push-Button Verification of File Systems via Crash Refinement. In Proceedings of the 12th Symposium on Operating Systems Design and Implementation (OSDI). Savannah, GA, USA, 1--16."},{"key":"e_1_3_2_1_50_1","unstructured":"Miri team. 2021. Miri. https:\/\/github.com\/rust-lang\/miri  Miri team. 2021. Miri. https:\/\/github.com\/rust-lang\/miri"},{"key":"e_1_3_2_1_51_1","volume-title":"Crux: Introducing our new open-source tool for software verification. https:\/\/galois.com\/blog\/2020\/10\/cruxintroducing-our-new-open-source-tool-for-software-verification\/","author":"Tomb Aaron","year":"2020","unstructured":"Aaron Tomb . 2020 . Crux: Introducing our new open-source tool for software verification. https:\/\/galois.com\/blog\/2020\/10\/cruxintroducing-our-new-open-source-tool-for-software-verification\/ Aaron Tomb. 2020. Crux: Introducing our new open-source tool for software verification. https:\/\/galois.com\/blog\/2020\/10\/cruxintroducing-our-new-open-source-tool-for-software-verification\/"},{"key":"e_1_3_2_1_52_1","unstructured":"Aaron Turon. 2015. Fearless Concurrency with Rust. https:\/\/blog.rustlang.org\/2015\/04\/10\/Fearless-Concurrency.html  Aaron Turon. 2015. Fearless Concurrency with Rust. https:\/\/blog.rustlang.org\/2015\/04\/10\/Fearless-Concurrency.html"},{"key":"e_1_3_2_1_53_1","unstructured":"Werner Vogels. 2021. Diving Deep on S3 Consistency. https:\/\/www.allthingsdistributed.com\/2021\/04\/s3-strong-consistency.html  Werner Vogels. 2021. Diving Deep on S3 Consistency. https:\/\/www.allthingsdistributed.com\/2021\/04\/s3-strong-consistency.html"},{"key":"e_1_3_2_1_54_1","volume-title":"Proceedings of the 7th Symposium on Operating Systems Design and Implementation (OSDI)","author":"Yang Junfeng","year":"2006","unstructured":"Junfeng Yang , Paul Twohey , Dawson Engler , and Madanlal Musuvathi . 2006 . eXplode: A Lightweight, General System for Finding Serious Storage System Errors . In Proceedings of the 7th Symposium on Operating Systems Design and Implementation (OSDI) . Seattle, WA, USA, 131--146. Junfeng Yang, Paul Twohey, Dawson Engler, and Madanlal Musuvathi. 2006. eXplode: A Lightweight, General System for Finding Serious Storage System Errors. In Proceedings of the 7th Symposium on Operating Systems Design and Implementation (OSDI). Seattle, WA, USA, 131--146."}],"event":{"name":"SOSP '21: ACM SIGOPS 28th Symposium on Operating Systems Principles","location":"Virtual Event Germany","acronym":"SOSP '21","sponsor":["SIGOPS ACM Special Interest Group on Operating Systems","USENIX Assoc USENIX Assoc"]},"container-title":["Proceedings of the ACM SIGOPS 28th Symposium on Operating Systems Principles"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3477132.3483540","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3477132.3483540","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:49:15Z","timestamp":1750193355000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3477132.3483540"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,10,26]]},"references-count":54,"alternative-id":["10.1145\/3477132.3483540","10.1145\/3477132"],"URL":"https:\/\/doi.org\/10.1145\/3477132.3483540","relation":{},"subject":[],"published":{"date-parts":[[2021,10,26]]},"assertion":[{"value":"2021-10-26","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}