{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,8]],"date-time":"2026-10-08T11:58:21Z","timestamp":1791460701721,"version":"4.3.4"},"reference-count":40,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2023,10,16]],"date-time":"2023-10-16T00:00:00Z","timestamp":1697414400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"NSF\/VMware Partnership on Software Defined Infrastructure as a Foundation for Clean-Slate Computing Security","award":["CNS-1700521"],"award-info":[{"award-number":["CNS-1700521"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2023,10,16]]},"abstract":"<jats:p>In concurrent verification, separation logic provides a strong story for handling both resources that are owned exclusively and resources that are shared persistently (i.e., forever). However, the situation is more complicated for temporarily shared state, where state might be shared and then later reclaimed as exclusive. We believe that a framework for temporarily-shared state should meet two key goals not adequately met by existing techniques. One, it should allow and encourage users to verify new sharing strategies. Two, it should provide an abstraction where users manipulate shared state in a way agnostic to the means with which it is shared.<\/jats:p>\n          <jats:p>We present Leaf, a library in the Iris separation logic which accomplishes both of these goals by introducing a novel operator, which we call guarding, that allows one proposition to represent a shared version of another. We demonstrate that Leaf meets these two goals through a modular case study: we verify a reader-writer lock that supports shared state, and a hash table built on top of it that uses shared state.<\/jats:p>","DOI":"10.1145\/3622798","type":"journal-article","created":{"date-parts":[[2023,10,16]],"date-time":"2023-10-16T15:41:29Z","timestamp":1697470889000},"page":"31-58","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Leaf: Modularity for Temporary Sharing in Separation Logic"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0009-0003-1104-7795","authenticated-orcid":false,"given":"Travis","family":"Hance","sequence":"first","affiliation":[{"name":"Carnegie Mellon University, Pittsburgh, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1781-2473","authenticated-orcid":false,"given":"Jon","family":"Howell","sequence":"additional","affiliation":[{"name":"VMware Research, Bellevue, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0006-4209-1635","authenticated-orcid":false,"given":"Oded","family":"Padon","sequence":"additional","affiliation":[{"name":"VMware Research, Palo Alto, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9113-1684","authenticated-orcid":false,"given":"Bryan","family":"Parno","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, Pittsburgh, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2023,10,16]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2018.03.016"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1047659.1040327"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44898-5_4"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2442516.2442532"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3037697.3037721"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_10"},{"key":"e_1_2_1_7_1","unstructured":"E. Clausen. 2017. Verifying Hash Tables in Iris. \t\t\t\t  E. Clausen. 2017. Verifying Hash Tables in Iris."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371102"},{"key":"e_1_2_1_9_1","volume-title":"Proceedings of the 2019 USENIX Conference on Usenix Annual Technical Conference (USENIX ATC \u201919)","author":"Dice Dave","year":"2019","unstructured":"Dave Dice and Alex Kogan . 2019 . BRAVO: Biased Locking for Reader-Writer Locks . In Proceedings of the 2019 USENIX Conference on Usenix Annual Technical Conference (USENIX ATC \u201919) . USENIX Association, USA. 315\u2013328. isbn:978 1939133038 Dave Dice and Alex Kogan. 2019. BRAVO: Biased Locking for Reader-Writer Locks. In Proceedings of the 2019 USENIX Conference on Usenix Annual Technical Conference (USENIX ATC \u201919). USENIX Association, USA. 315\u2013328. isbn:9781939133038"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429104"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14107-2_24"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10672-9_13"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3301501"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.8327489"},{"key":"e_1_2_1_15_1","volume-title":"Leaf: Modularity for Temporary Sharing in Separation Logic (Extended Version). https:\/\/doi.org\/10.48550\/arXiv.2309.04851","author":"Hance Travis","year":"2023","unstructured":"Travis Hance , Jon Howell , Oded Padon , and Bryan Parno . 2023 . Leaf: Modularity for Temporary Sharing in Separation Logic (Extended Version). https:\/\/doi.org\/10.48550\/arXiv.2309.04851 10.48550\/arXiv.2309.04851 Travis Hance, Jon Howell, Oded Padon, and Bryan Parno. 2023. Leaf: Modularity for Temporary Sharing in Separation Logic (Extended Version). https:\/\/doi.org\/10.48550\/arXiv.2309.04851"},{"key":"e_1_2_1_16_1","volume-title":"Sharding the State Machine: Automated Modular Reasoning for Complex Concurrent Systems. In 17th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2023","author":"Hance Travis","year":"2023","unstructured":"Travis Hance , Yi Zhou , Andrea Lattuada , Reto Achermann , Alex Conway , Ryan Stutsman , Gerd Zellweger , Chris Hawblitzel , Jon Howell , and Bryan Parno . 2023 . Sharding the State Machine: Automated Modular Reasoning for Complex Concurrent Systems. In 17th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2023 , Boston, MA, USA , July 10-12, 2023, Roxana Geambasu and Ed Nightingale (Eds.). USENIX Association, 911\u2013929. https:\/\/www.usenix.org\/conference\/osdi23\/presentation\/hance Travis Hance, Yi Zhou, Andrea Lattuada, Reto Achermann, Alex Conway, Ryan Stutsman, Gerd Zellweger, Chris Hawblitzel, Jon Howell, and Bryan Parno. 2023. Sharding the State Machine: Automated Modular Reasoning for Complex Concurrent Systems. In 17th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2023, Boston, MA, USA, July 10-12, 2023, Roxana Geambasu and Ed Nightingale (Eds.). USENIX Association, 911\u2013929. https:\/\/www.usenix.org\/conference\/osdi23\/presentation\/hance"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547647"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/IPPS.1992.222989"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28869-2_19"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158154"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951943"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676980"},{"key":"e_1_2_1_24_1","volume-title":"Proceedings of the USENIX Annual Technical Conference (USENIX ATC \u201917)","author":"Kashyap Sanidhya","year":"2017","unstructured":"Sanidhya Kashyap , Changwoo Min , and Taesoo Kim . 2017 . Scalable NUMA-Aware Blocking Synchronization Primitives . In Proceedings of the USENIX Annual Technical Conference (USENIX ATC \u201917) . USENIX Association, USA. 603\u2013615. isbn:978 1931971386 Sanidhya Kashyap, Changwoo Min, and Taesoo Kim. 2017. Scalable NUMA-Aware Blocking Synchronization Primitives. In Proceedings of the USENIX Annual Technical Conference (USENIX ATC \u201917). USENIX Association, USA. 603\u2013615. isbn:9781931971386"},{"key":"e_1_2_1_25_1","volume-title":"The Art of Computer Programming","author":"Knuth Donald E.","unstructured":"Donald E. Knuth . 1998. The Art of Computer Programming , Volume 3: (2nd Ed.) Sorting and Searching. Addison Wesley Longman Publishing Co., Inc., USA. isbn: 0201896850 Donald E. Knuth. 1998. The Art of Computer Programming, Volume 3: (2nd Ed.) Sorting and Searching. Addison Wesley Longman Publishing Co., Inc., USA. isbn:0201896850"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_26"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2364527.2364536"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429134"},{"key":"e_1_2_1_29_1","volume-title":"Proceedings of the USENIX Annual Technical Conference (USENIX ATC\u201914)","author":"Liu Ran","year":"2014","unstructured":"Ran Liu , Heng Zhang , and Haibo Chen . 2014 . Scalable Read-Mostly Synchronization Using Passive Reader-Writer Locks . In Proceedings of the USENIX Annual Technical Conference (USENIX ATC\u201914) . USENIX Association, USA. 219\u2013230. isbn:978 1931971102 Ran Liu, Heng Zhang, and Haibo Chen. 2014. Scalable Read-Mostly Synchronization Using Passive Reader-Writer Locks. In Proceedings of the USENIX Annual Technical Conference (USENIX ATC\u201914). USENIX Association, USA. 219\u2013230. isbn:9781931971102"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_16"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.035"},{"key":"e_1_2_1_32_1","volume-title":"Local Reasoning for Java. Ph. D. Dissertation","author":"Parkinson Matthew","unstructured":"Matthew Parkinson . 2005. Local Reasoning for Java. Ph. D. Dissertation . University of Cambridge . Matthew Parkinson. 2005. Local Reasoning for Java. Ph. D. Dissertation. University of Cambridge."},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-017-0435-1"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3018610.3018624"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_2_1_36_1","unstructured":"John C. Reynolds. 2008. An Introduction to Separation Logic. https:\/\/www.cs.cmu.edu\/~jcr\/copenhagen08.pdf Accessed: 2022-11-08 \t\t\t\t  John C. Reynolds. 2008. An Introduction to Separation Logic. https:\/\/www.cs.cmu.edu\/~jcr\/copenhagen08.pdf Accessed: 2022-11-08"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2312005.2312015"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_9"},{"key":"e_1_2_1_39_1","unstructured":"The cppreference Team. 2011. std::lock_guard. https:\/\/en.cppreference.com\/w\/cpp\/thread\/lock_guard Accessed: 2022-11-08 \t\t\t\t  The cppreference Team. 2011. std::lock_guard. https:\/\/en.cppreference.com\/w\/cpp\/thread\/lock_guard Accessed: 2022-11-08"},{"key":"e_1_2_1_40_1","unstructured":"The Rust Team. 2014. Struct std::sync::RwLockReadGuard. https:\/\/doc.rust-lang.org\/std\/sync\/struct.RwLockReadGuard.html Accessed: 2022-11-08 \t\t\t\t  The Rust Team. 2014. Struct std::sync::RwLockReadGuard. https:\/\/doc.rust-lang.org\/std\/sync\/struct.RwLockReadGuard.html Accessed: 2022-11-08"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3622798","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3622798","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:37:04Z","timestamp":1750178224000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3622798"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,10,16]]},"references-count":40,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2023,10,16]]}},"alternative-id":["10.1145\/3622798"],"URL":"https:\/\/doi.org\/10.1145\/3622798","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,10,16]]},"assertion":[{"value":"2023-10-16","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}