{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T11:09:43Z","timestamp":1784200183917,"version":"3.55.0"},"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% 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":10,"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_3_2_2_2","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_3_2_3_2","unstructured":"Unsafe Code Guidelines Issue #248. 2020. Stacked Borrows: track raw pointers more precisely. https:\/\/github.com\/rustlang\/unsafe-code-guidelines\/issues\/248."},{"key":"e_1_3_2_4_2","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_3_2_5_2","unstructured":"Unsafe Code Guidelines Issue #273. 2021. Stacked Borrows: using the topmost \"untagged\" item is not \"monotonic\". https:\/\/github.com\/rust-lang\/unsafe-code-guidelines\/issues\/273."},{"key":"e_1_3_2_6_2","unstructured":"Miri Issue #3082. 2023. Is a stacked borrows error in iced-x86 a problem?\u00a0. https:\/\/github.com\/rust-lang\/miri\/issues\/3082."},{"key":"e_1_3_2_7_2","unstructured":"Miri Issue #3657. 2024. Possible false positive of stacked borrow rules. https:\/\/github.com\/rust-lang\/miri\/issues\/3657."},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/3674652"},{"key":"e_1_3_2_9_2","unstructured":"Anton Fetisov. 2024. Aliasing of raw pointers. https:\/\/internals.rust-lang.org\/t\/aliasing-of-raw-pointers\/21746."},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1145\/3498689"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737979"},{"key":"e_1_3_2_12_2","unstructured":"ISO.2017. C17 Standard. ISO\/IEC 9899:2018."},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/3371109"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2738005"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-03545-1_4"},{"key":"e_1_3_2_17_2","volume-title":"The C standard formalized in Coq. Ph.D. Dissertation","author":"Krebbers Robbert","year":"2015","unstructured":"Robbert Krebbers. 2015. The C standard formalized in Coq. Ph.D. Dissertation. Radboud University Nijmegen. https:\/\/robbertkrebbers.nl\/thesis.html"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/3236772"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/3276495"},{"key":"e_1_3_2_20_2","volume-title":"The CompCert memory model, version 2. Technical Report RR-7987","author":"Leroy Xavier","year":"2012","unstructured":"Xavier Leroy, Andrew Appel, Sandrine Blazy, and Gordon Stewart. 2012. The CompCert memory model, version 2. Technical Report RR-7987. Inria. https:\/\/hal.inria.fr\/hal-00703441"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-008-9099-0"},{"key":"e_1_3_2_22_2","first-page":"65","article-title":"Alive2: Bounded Translation Validation for LLVM","author":"Lopes Nuno P","year":"2021","unstructured":"Nuno P Lopes, Juneyoung Lee, Chung-Kil Hur, Zhengyang Liu, and John Regehr. 2021. Alive2: Bounded Translation Validation for LLVM. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation. 65\u201379.","journal-title":"Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation"},{"key":"e_1_3_2_23_2","unstructured":"Dani\u0451l Louwrink. 2021. A Separation Logic for Stacked Borrows. Master\u2019s thesis. https:\/\/eprints.illc.uva.nl\/id\/eprint\/1790\/."},{"key":"e_1_3_2_24_2","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). https:\/\/arxiv.org\/abs\/2404.11671."},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/3290380"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908081"},{"key":"e_1_3_2_27_2","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_3_2_28_2","volume-title":"C formalised in HOL. Ph.D. Dissertation","author":"Norrish Michael","year":"1998","unstructured":"Michael Norrish. 1998.\u00a0C formalised in HOL. Ph.D. Dissertation. University of Cambridge."},{"key":"e_1_3_2_29_2","unstructured":"LLVM Project. 2024. LLVM Language Reference. https:\/\/llvm.org\/docs\/LangRef.html."},{"key":"e_1_3_2_30_2","unstructured":"The Coq Team. 2023. The Coq proof assistant. https:\/\/coq.inria.fr\/."},{"key":"e_1_3_2_31_2","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_3_2_32_2","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 10.5281\/zenodo.15002703 (latest version available on paper website: https:\/\/plf.inf.ethz.ch\/research\/pldi25-tree-borrows.html).","DOI":"10.5281\/zenodo.15002703"},{"key":"e_1_3_2_33_2","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":[[2026,7,16]],"date-time":"2026-07-16T10:09:55Z","timestamp":1784196595000},"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":"2024-11-15","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-03-06","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-06-13","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}