7 ms·
Tree Borrows
- pvg 1y agoThe Stacked Borrows mentioned had threads in 2020 and 2018 https://news.ycombinator.com/item?id=22281205 https://news.ycombinator.com/item?id=22281205 https://news.ycombinator.com/item?id=17715399 https://news.ycombinator.com/item?id=17715399
- kibwen 1y agoRecent blog post from Ralf Jung providing some extra context: https://www.ralfj.de/blog/2025/07/07/tree-borrows-paper.html https://www.ralfj.de/blog/2025/07/07/tree-borrows-paper.html Bonus: recent talk from Ralf Jung on his group's efforts to precisely specify Rust's operational semantics in executable form in a dialect of Rust: https://youtube.com/watch?v=yoeuW_dSe0o https://youtube.com/watch?v=yoeuW_dSe0o
- wavemode 1y agoFrom the paper: > The problem with unsafe code is that it can do things like this: fn main() { let mut x = 42; let ptr = &mut x as *mut i32; let val = unsafe { write_both(&mut *ptr, &mut *ptr) }; println!("{val}"); } No it can't? Using pointers to coexist multiple mutable references to the same variable is undefined behavior. Unless I'm just misunderstanding the point they're trying to make here.
- seritools 1y ago"can do things" in this case doesn't mean "is allowed to do things". "Unsafe code allows to express the following, which is UB:"
- deleted 1y ago[deleted]
- ehsanu1 1y agoI believe that's exactly the point: it's too easy to violate constraints like not allowing multiple mutable references. Unsafe is meant for cases where the validity of the code is difficult to prove with rust's lifetime analysis, but can be abused to do much more than that.
- pavpanchekha 1y agoThe point of this work is to pin down the exact boundaries of undefined behavior. Certainly the code above is accepted by the Rust compiler, but it also breaks rules. What rules? In essence, we know that: - Anything accepted by the borrow checker is legal - Unsafe can express illegal / undefined behavior - There's some set of rules, broader than what the borrow checker can check, that is still legal / defined behavior The goal of this line of work is to precisely specify that set of rules. The outlines are clear (basically, no writable pointers should alias) but the details (interior pointers, invalidation of iterators, is it creating or using bad pointers that's bad, etc) are really hard. The previous paper in this series, on Stacked Borrows, was simpler but more restrictive, and real-world unsafe code often failed its rules (while still seeming correct). Tree Borrows is broader and allows more while still being provably safe.
- ralfj 1y ago> allows more while still being provably safe. Note that we have not yet proven this. :) I hope to one day prove that every program accepted by the borrow checker is compatible with TB, but right now, that is only a (very well-tested) conjecture.
- sunshowers 1y agoHi Ralf! Congrats to you all for the PLDI distinguished paper award.
- ralfj 1y agoThanks :-)
- oconnor663 1y agoYou're already getting a lot of replies, and I don't want to pile on, but I think the clearest way to see the intent there is at the start of the following paragraph: > Given that aliasing optimizations are something that the Rust compiler developers clearly want to support, we need some way of “ruling out” counterexamples like the one above from consideration.
- ralfj 1y ago> Using pointers to coexist multiple mutable references to the same variable is undefined behavior. Yes, but which exact rule does it violate? What is the exact definition that says that it is UB? Tree Borrows is a proposal for exactly such a definition. "code can do things like this" here means "you can write this code and compile it and run it and it will do something, and unless we have something like Tree Borrows we have no argument for why there would be anything wrong with this code". You seem to have already accepted that we need something like Tree Borrows (i.e., we should say code like this is UB). This part of the paper is arguing why we need something like Tree Borrows. :)
- deleted 1y ago[deleted]
- GolDDranks 1y ago> Unless I'm just misunderstanding the point they're trying to make here. You misunderstand the word "can". Yes, you can, in unsafe code, do that. And yes, that is undefined behaviour ;) https://play.rust-lang.org/?version=stable&mode=debug&edition=2024&gist=a26f2187871532909356b02735644f1b https://play.rust-lang.org/?version=stable&mode=debug&editio...
- pil0u 1y agoJust realised that one of the author, Neven Villani, is Cédric Villani's (Fields Medal 2010) son. Apples don't fall far from the tree, indeed.
- fuhsnn 1y agoI wonder if Rust or future PL would evolve into allowing multiple borrow checker implementations with varying characteristics (compile speed, runtime speed, algorithm flexibility, etc.) that projects can choose from.
- speed_spread 1y agoI cannot imagine how that would work. You couldn't combine code that expect different borrowing rules to be applied. You'd effectively be creating as many sub-dialects as there are borrow checker implementations.
- vlovich123 1y agoFWIW technically the rules are the same. How they go about proving that the rules are upheld for a program is what would be different.
- School-Cotton 1y agoWhat’s wrong with the compile or runtime speed of the current one?
- pjmlp 1y agoWe already have that by having multiple approaches via affine types (what Rust uses), linear types, effects, dependent types, formal proofs. All have different costs and capabilities across implementation, performance and developer experience. Then we have what everyone else besides Rust is actually going for, the productivity of automatic resource management (regardless of how), coupled with one of the type systems above, only for performance critical code paths.
- LelouBil 1y agoI would love some sort of affine types in languages like Kotlin, it just makes cleaner code organization in my opinion. Doesn't matter if it's purely "syntaxical" because the language is garbage collected, just the fact of specifying what owns what and be explicit about multiple references is great imo. Some sort of effects systems can already be simulated with Kotlin features too. Programming language theory is so interesting!
- Voultapher 1y agoAmazing work, I remember reading the Tree Borrows spec? on Nevin's website a couple years ago and being thoroughly impressed by how it solves some pretty gnarly issue quite elegantly. And in my experience [1] [2] it does indeed allow for sensible code that is illegal under Stacked Borrows. [1] https://github.com/Voultapher/sort-research-rs/blob/main/writeup/sort_safety/text.md#property-analysis https://github.com/Voultapher/sort-research-rs/blob/main/wri... Miri column [2] https://github.com/rust-lang/rust/blob/6b3ae3f6e45a33c2d95fa0362c9b2593e567fd34/library/core/src/slice/sort/unstable/quicksort.rs#L298 https://github.com/rust-lang/rust/blob/6b3ae3f6e45a33c2d95fa...
- vollbrecht 1y agoHmm i just tested out the claim that the following rust code would be rejected ( Example 4 in the paper). And it seams to not be the case on the stable compiler version? fn write(x: &mut i32) {*x = 10} fn main() { let x = &mut 0; let y = x as *mut i32; //write(x); // this should use the mention implicit twophase borrow *x = 10; // this should not and therefore be rejected by the compiler unsafe {*y = 15 }; }
- Arnavion 1y agoStacked borrows is miri's runtime model. Run it under miri and you will see the error reported for the `*x = 10;` version but not the `write(x);` version - "Undefined Behavior: attempting a write access using [...] but that tag does not exist in the borrow stack for this location". rustc itself has no reason to reject either version, because y is a *mut and thus has no borrow/lifetime relation to the &mut that x is, from a compile-time/typesystem perspective.
- vollbrecht 1y agoAh that make sense. Thanks for clarifying.
- haberman 1y agoThe paper mentions that the authors implemented tree borrows in Miri. Is this change likely to be adopted by Miri as the default model going forward?
- ethan_smith 1y agoThe paper is describing the behavior under the proposed Tree Borrows model, not the current borrow checker implementation which uses a more limited analysis that doesn't detect this particular conflict between the raw pointer and mutable reference.
- jcalvinowens 1y ago> On the one hand, compilers would like to exploit the strong guarantees of the type system—particularly those pertaining to aliasing of pointers—in order to unlock powerful intraprocedural optimizations. How true is this really? Torvalds has argued for a long time that strict aliasing rules in C are more trouble than they're worth, I find his arguments compelling. Here's one of many examples: https://lore.kernel.org/all/CAHk-=wgq1DvgNVoodk7JKc6BuU1m9UnoN+k=TLtxCAL7xTP=Dg@mail.gmail.com/ https://lore.kernel.org/all/CAHk-=wgq1DvgNVoodk7JKc6BuU1m9Un... (the entire thread worth reading if you find this sort of thing interesting) Is Rust somehow fundamentally different? Based on limited experience, it seems not (at least, when unsafe is involved...).
- ralfj 1y agoI would agree that C's strict aliasing rules are terrible. The rules we are proposing for Rust are very different. They are both more useful for compilers and, in my opinion, less onerous for programmers. We also have an actual in-language opt-out: use raw pointers. And finally, we have a tool you can use to check your code. But in the end, it's a trade-off, like everything in language design. (In life, really. ;) We think that in Rust we may have found a new sweet spot for this kind of optimizations. Time will tell whether we are right.
- kookamamie 1y agoAgreed about C's aliasing rules. Fortran had a better set of defaults.
- NobodyNada 1y agoAs someone who has been writing a lot of unsafe Rust (mostly in an embedded context), I'm thrilled about and thankful for the work that you, your students, and the opsem team are doing. When you're working with anything below the application level, C's confusing and underspecified rules about UB are almost impossible to keep track of, especially when it comes to aliasing and volatile/MMIO. The spec is so difficult to read and full of complicated cross-references that to actually get a practical answer you have to look for a random Stack Overflow post that may or may not have a correct interpretation of the spec, and may or may not address your specific problem. Rust right now feels a lot harder to work with, because the spec isn't done. When you have a concrete question about a piece of code, like "is this conversion from an &mut to a *mut and back sound", and you try to look for documentation on it, you get either "Nobody knows, Rust aliasing model isn't defined"; a hand-wavy explanation that is not rigorous or specific; or a model like Stack Borrows or Tree Borrows that's defined a little too formally for easy digestion :) But when I really started digging, I realized just how much cleaner Rust's semantics are. References aren't actually hard, Tree Borrows basically boils down to "while an &mut reference is live, you can only access the value through pointers or references derived from that reference". Pointer operations have straightforward semantics, there's no confusing notions of typed memory, and no UB "just because" for random things like integer overflow. It's just so much less complicated to understand than C's abstract machine. I'm really looking forward to things like MiniRust, and to an aliasing model making it into the Reference / other documentation, because at that point I feel like unsafe Rust will be way easier to write confidently and correctly than C. Congrats on the publication, and thanks again for the work you all have put into this.
- gavinhoward 1y agoThis looks excellent. I will probably implement this model for my own language.
- b0a04gl 1y ago[dead]
- Nurbek-F 1y agoIt can't be a dejavu. I keep seeing this post every 2-3 months...
- steveklabnik 1y agoThe paper is years in the making. This is it finally being published.
- deleted 1y ago[deleted]
- olddustytrail 1y ago_Tree Borrows_ "I want my fuckin' money back." "Hoom, hmm, let us not be hasty!" "You got 48 hours to deliver or the sapling gets it, Treebeard."
- nixpulvis 1y agoHere's the implementation in Miri for those interested: https://github.com/rust-lang/miri/tree/master/src/borrow_tracker/tree_borrows https://github.com/rust-lang/miri/tree/master/src/borrow_tra...
- deleted 1y ago[deleted]
- chombier 1y agoThe PLDI talk is also available: https://www.youtube.com/watch?v=CJi_Fcs4bak https://www.youtube.com/watch?v=CJi_Fcs4bak
- jojomodding 1y agoThanks, I added it to the website.