{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:45:52Z","timestamp":1780994752868,"version":"3.54.1"},"reference-count":32,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,6,10]]},"abstract":"<jats:p>\n            The Rust programming language is well known for its ownership-based type system, which offers strong guarantees like memory safety and data race freedom. However, Rust also provides\n            <jats:italic toggle=\"yes\">unsafe<\/jats:italic>\n            escape hatches, for which safety is not guaranteed automatically and must instead be manually upheld by the programmer. This creates a tension. On the one hand, compilers would like to exploit the strong guarantees of the type system\u2014particularly those pertaining to aliasing of pointers\u2014in order to unlock powerful intraprocedural optimizations. On the other hand, those optimizations are easily invalidated by \u201cbadly behaved\u201d unsafe code. To ensure correctness of such optimizations, it thus becomes necessary to clearly define what unsafe code is \u201cbadly behaved.\u201d In prior work,\n            <jats:italic toggle=\"yes\">Stacked Borrows<\/jats:italic>\n            defined a set of rules achieving this goal. However, Stacked Borrows rules out several patterns that turn out to be common in real-world unsafe Rust code, and it does not account for advanced features of the Rust borrow checker that were introduced more recently.\n          <\/jats:p>\n          <jats:p>\n            To resolve these issues, we present\n            <jats:italic toggle=\"yes\">Tree Borrows<\/jats:italic>\n            . As the name suggests, Tree Borrows is defined by replacing the stack at the heart of Stacked Borrows with a tree. This overcomes the aforementioned limitations: our evaluation on the 30 000 most widely used Rust crates shows that Tree Borrows rejects 54\u202f% fewer test cases than Stacked Borrows does. Additionally, we prove (in Rocq) that it retains most of the Stacked Borrows optimizations and also enables important new ones, notably read-read reorderings.\n          <\/jats:p>","DOI":"10.1145\/3735592","type":"journal-article","created":{"date-parts":[[2025,6,13]],"date-time":"2025-06-13T16:02:27Z","timestamp":1749830547000},"page":"1019-1042","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":8,"title":["Tree Borrows"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2726-5036","authenticated-orcid":false,"given":"Neven","family":"Villani","sequence":"first","affiliation":[{"name":"Univ. Grenoble Alpes - CNRS - Grenoble INP (Institute of Engineering), Grenoble, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5038-8283","authenticated-orcid":false,"given":"Johannes","family":"Hostert","sequence":"additional","affiliation":[{"name":"ETH Zurich, Z\u00fcrich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3884-6867","authenticated-orcid":false,"given":"Derek","family":"Dreyer","sequence":"additional","affiliation":[{"name":"MPI-SWS, Saarbr\u00fccken, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7669-6348","authenticated-orcid":false,"given":"Ralf","family":"Jung","sequence":"additional","affiliation":[{"name":"ETH Zurich, Z\u00fcrich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,6,13]]},"reference":[{"key":"e_1_2_2_1_1","volume-title":"Code Guidelines Issue '134","author":"Unsafe","year":"2019","unstructured":"Unsafe Code Guidelines Issue '134. 2019. Stacked Borrows: raw pointer usable only for T too strict? https:\/\/github.com\/rust-lang\/unsafe-code-guidelines\/issues\/134"},{"key":"e_1_2_2_2_1","volume-title":"Code Guidelines Issue '248","author":"Unsafe","year":"2020","unstructured":"Unsafe Code Guidelines Issue '248. 2020. Stacked Borrows: track raw pointers more precisely. https:\/\/github.com\/rust-lang\/unsafe-code-guidelines\/issues\/248"},{"key":"e_1_2_2_3_1","volume-title":"Code Guidelines Issue '256","author":"Unsafe","year":"2020","unstructured":"Unsafe Code Guidelines Issue '256. 2020. Storing an object as &Header, but reading the data past the end of the header. https:\/\/github.com\/rust-lang\/unsafe-code-guidelines\/issues\/256"},{"key":"e_1_2_2_4_1","volume-title":"Code Guidelines Issue '273","author":"Unsafe","year":"2021","unstructured":"Unsafe Code Guidelines Issue '273. 2021. Stacked Borrows: using the topmost \u00fcntagged\" item is not \"monotonic\". https:\/\/github.com\/rust-lang\/unsafe-code-guidelines\/issues\/273"},{"key":"e_1_2_2_5_1","volume-title":"Issue '3082","author":"Miri","year":"2023","unstructured":"Miri Issue '3082. 2023. Is a stacked borrows error in iced-x86 a problem? https:\/\/github.com\/rust-lang\/miri\/issues\/3082"},{"key":"e_1_2_2_6_1","volume-title":"Issue '3657","author":"Miri","year":"2024","unstructured":"Miri Issue '3657. 2024. Possible false positive of stacked borrow rules. https:\/\/github.com\/rust-lang\/miri\/issues\/3657"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3674652"},{"key":"e_1_2_2_8_1","unstructured":"Anton Fetisov. 2024. Aliasing of raw pointers. https:\/\/internals.rust-lang.org\/t\/aliasing-of-raw-pointers\/21746"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498689"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737979"},{"key":"e_1_2_2_11_1","first-page":"2018","article-title":"C17 Standard","volume":"9899","author":"ISO.","year":"2017","unstructured":"ISO. 2017. C17 Standard. ISO\/IEC 9899:2018","journal-title":"ISO\/IEC"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371109"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","unstructured":"Jeehoon Kang Chung-Kil Hur William Mansky Dmitri Garbuzov Steve Zdancewic and Viktor Vafeiadis. 2015. A formal C memory model supporting integer-pointer casts. In PLDI. 326\u2013335. https:\/\/doi.org\/10.1145\/2737924.2738005 10.1145\/2737924.2738005","DOI":"10.1145\/2737924.2738005"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-03545-1_4"},{"key":"e_1_2_2_16_1","volume-title":"The C standard formalized in Coq. Ph. D. Dissertation","author":"Krebbers Robbert","unstructured":"Robbert Krebbers. 2015. The C standard formalized in Coq. Ph. D. Dissertation. Radboud University Nijmegen. https:\/\/robbertkrebbers.nl\/thesis.html"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236772"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276495"},{"key":"e_1_2_2_19_1","unstructured":"Xavier Leroy Andrew Appel Sandrine Blazy and Gordon Stewart. 2012. The CompCert memory model version 2. Inria. https:\/\/hal.inria.fr\/hal-00703441"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-008-9099-0"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454030"},{"key":"e_1_2_2_22_1","unstructured":"Dani\u00ebl Louwrink. 2021. A Separation Logic for Stacked Borrows. Master\u2019s thesis. https:\/\/eprints.illc.uva.nl\/id\/eprint\/1790\/"},{"key":"e_1_2_2_23_1","volume-title":"A Study of Undefined Behavior Across Foreign Function Boundaries in Rust Libraries. CoRR, abs\/2404.11671","author":"McCormack Ian","year":"2024","unstructured":"Ian McCormack, Joshua Sunshine, and Jonathan Aldrich. 2024. A Study of Undefined Behavior Across Foreign Function Boundaries in Rust Libraries. CoRR, abs\/2404.11671 (2024), arxiv:2404.11671"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290380"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","unstructured":"Kayvan Memarian Justus Matthiesen James Lingard Kyndylan Nienhuis David Chisnall Robert N. M. Watson and Peter Sewell. 2016. Into the depths of C: Elaborating the de facto standards. In PLDI. 1\u201315. https:\/\/doi.org\/10.1145\/2908080.2908081 10.1145\/2908080.2908081","DOI":"10.1145\/2908080.2908081"},{"key":"e_1_2_2_26_1","volume-title":"N2014: What is C in practice? (Cerberus survey v2): Analysis of Responses. ISO SC22 WG14 N2014","author":"Memarian Kayvan","year":"2016","unstructured":"Kayvan Memarian and Peter Sewell. 2016. N2014: What is C in practice? (Cerberus survey v2): Analysis of Responses. ISO SC22 WG14 N2014,. http:\/\/www.cl.cam.ac.uk\/ pes20\/cerberus\/notes50-survey-discussion.html"},{"key":"e_1_2_2_27_1","volume-title":"C formalised in HOL. Ph. D. Dissertation","author":"Norrish Michael","unstructured":"Michael Norrish. 1998. C formalised in HOL. Ph. D. Dissertation. University of Cambridge."},{"key":"e_1_2_2_28_1","unstructured":"LLVM Project. 2024. LLVM Language Reference. https:\/\/llvm.org\/docs\/LangRef.html"},{"key":"e_1_2_2_29_1","unstructured":"The Coq Team. 2023. The Coq proof assistant. https:\/\/coq.inria.fr\/"},{"key":"e_1_2_2_30_1","unstructured":"The Rust Team. 2020. Rust Compiler Development Guide: Two-phase borrows. https:\/\/rustc-dev-guide.rust-lang.org\/borrow_check\/two_phase_borrows.html"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","unstructured":"Neven Villani Johannes Hostert Derek Dreyer and Ralf Jung. 2025. Tree Borrows \u2013 Artifact. https:\/\/doi.org\/10.5281\/zenodo.15002703 (latest version available on paper website: 10.5281\/zenodo.15002703","DOI":"10.5281\/zenodo.15002703"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473572"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3735592","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,16]],"date-time":"2025-07-16T06:09:05Z","timestamp":1752646145000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3735592"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,6,10]]},"references-count":32,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2025,6,10]]}},"alternative-id":["10.1145\/3735592"],"URL":"https:\/\/doi.org\/10.1145\/3735592","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,6,10]]},"assertion":[{"value":"2025-06-13","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}