←back to thread

Tree Borrows

(plf.inf.ethz.ch)
565 points zdw | 2 comments | | HN request time: 0.45s | source
Show context
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 #
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 #
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 #
1. sunshowers ◴[] No.44512861[source]
Hi Ralf! Congrats to you all for the PLDI distinguished paper award.
replies(1): >>44513274 #
2. ralfj ◴[] No.44513274[source]
Thanks :-)