> 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.
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
pvg · 3h ago
The Stacked Borrows mentioned had threads in 2020 and 2018
Amazing 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.
Hmm 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 · 1h ago
Stacked 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 · 49m ago
Ah that make sense. Thanks for clarifying.
wavemode · 3h ago
From 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.
pavpanchekha · 2h ago
The 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 · 2h 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 · 40m ago
Hi Ralf! Congrats to you all for the PLDI distinguished paper award.
ralfj · 43s ago
Thanks :-)
ralfj · 2h 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. :)
GolDDranks · 1h 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 ;)
You'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.
ehsanu1 · 2h ago
I 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.
seritools · 3h 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:"
No comments yet
fuhsnn · 1h ago
I 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.
pjmlp · 1h ago
We 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 · 1h ago
I 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!
0x000xca0xfe · 1h ago
As I understand it the borrow checker only has false negatives but no false positives, correct?
Maybe a dumb question but couldn't you just run multiple implementations in parallel threads and whichever finishes first with a positive result wins?
vlovich123 · 31m ago
This presumes that checking composes which may not if you have orthogonal checker implementations. You might end up risking accepting an invalid program because part of it is valid under one checker, part under another, but the combination isn't actually valid. But maybe that's not actually possible in practice.
sunshowers · 41m ago
That would result in ecosystem splitting, which isn't great.
umanwizard · 1h ago
What’s wrong with the compile or runtime speed of the current one?
speed_spread · 1h ago
I 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 · 29m ago
FWIW technically the rules are the same. How they go about proving that the rules are upheld for a program is what would be different.
pil0u · 1h ago
Just 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.
tandr · 1h ago
> Apples don't fall far from the tree, indeed.
And one could say that they borrow from the tree some of their qualities. Sorry, couldn't resist.
Yoric · 1h ago
Hey, I used to have an office close to the dad's :)
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-=wgq1DvgNVoodk7JKc6BuU1m9Un...
Is Rust somehow fundamentally different? Based on limited experience, it seems not (at least, when unsafe is involved...).
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://news.ycombinator.com/item?id=22281205
https://news.ycombinator.com/item?id=17715399
[1] https://github.com/Voultapher/sort-research-rs/blob/main/wri... Miri column
[2] https://github.com/rust-lang/rust/blob/6b3ae3f6e45a33c2d95fa...
And it seams to not be the case on the stable compiler version?
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.
> The problem with unsafe code is that it can do things like this:
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.- 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.
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.
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. :)
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&editio...
> 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.
"Unsafe code allows to express the following, which is UB:"
No comments yet
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.
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!
Maybe a dumb question but couldn't you just run multiple implementations in parallel threads and whichever finishes first with a positive result wins?
And one could say that they borrow from the tree some of their qualities. Sorry, couldn't resist.
That's before he went into politics, though.