Most active commenters
  • ralfj(3)

←back to thread

Tree Borrows

(plf.inf.ethz.ch)
565 points zdw | 12 comments | | HN request time: 1.076s | source | bottom
1. wavemode ◴[] No.44511091[source]
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.
replies(6): >>44511182 #>>44511227 #>>44511321 #>>44511369 #>>44511392 #>>44512352 #
2. seritools ◴[] No.44511182[source]
"can do things" in this case doesn't mean "is allowed to do things".

"Unsafe code allows to express the following, which is UB:"

replies(1): >>44511268 #
3. ehsanu1 ◴[] No.44511227[source]
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.
4. ◴[] No.44511268[source]
5. pavpanchekha ◴[] No.44511321[source]
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.

replies(1): >>44511416 #
6. oconnor663 ◴[] No.44511369[source]
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.

7. ralfj ◴[] No.44511392[source]
> 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. :)

replies(1): >>44518867 #
8. ralfj ◴[] No.44511416[source]
> 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.

replies(1): >>44512861 #
9. GolDDranks ◴[] No.44512352[source]
> 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&editio...

10. sunshowers ◴[] No.44512861{3}[source]
Hi Ralf! Congrats to you all for the PLDI distinguished paper award.
replies(1): >>44513274 #
11. ralfj ◴[] No.44513274{4}[source]
Thanks :-)
12. ◴[] No.44518867[source]