5 ms·

It seems to me that there are three pieces we'd like to have, to show that we can trust Rust's borrow checker as much as we'd like to: - a runtime model of a h

It seems to me that there are three pieces we'd like to have, to show that we can trust Rust's borrow checker as much as we'd like to: - a runtime model of a hypothetical dialect of Rust without a borrow checker, defining which programs have undefined behaviour because they access memory "wrongly"; - a compiler for that dialect, in practice built on LLVM, that gives LLVM permission to invoke undefined behaviour only in cases where the model says that's allowed; - a demonstration that any program in the hypothetical dialect that can invoke undefined behaviour either uses `unsafe` or is rejected by the borrow checker. As I understand it, this paper is a plan for providing the first, and the compiler people think it's possible to use it to provide the second. Has the third been done, or is someone working on it?

zozbot234 7y ago
> Has the third been done, or is someone working on it? There has been a lot of work on this as part of the RustBelt project (that the OP is also a part of). But it's not "done" in any sense, for example traits are still unmodeled and a lot of the unsoundness of some kind or another that's been found in Rust has to do with them. The first goal is being worked on implicitly by the 'Rustonomicon' folks, who are trying to characterize "unsafe" Rust properly. Unsafe Rust is not "free of the borrow checker" in practice, but it's the part of the language that lets you do things which might be UB. So the two are obviously related.
viraptor 7y ago
> Has the third been done, or is someone working on it? Can this be done though? The way I understand this: Either 1. the whole model is specified and can be proven, (which wouldn't need the second step) or 2. you can only find specific counter-examples, not demonstrate there aren't any. (That would be like a solution to the halting problem) Did I miss something?
- mjw1007 7y ago
  If you're trying to analyse a program statically and find some property of its runtime behaviour, the halting problem only gets in the way when you need to be accurate about both whether the runtime behaviour does or doesn't have the property. Here, it's OK if the borrow checker rejects some programs which the stacked-borrows runtime model would say don't in fact invoke undefined behaviour, so long as it doesn't accept any which do. (And it surely will give some rejections of that sort, for example if I violate the borrowing rules in a function which is never called.)
  - kd5bjo 7y ago
    Also, this is the primary reason that unsafe exists— there exists code that is both useful and correct but the borrow checker can’t properly verify. It’s a marker that tells the compiler it’s not responsible for verifying that code.
    - smaddox 7y ago
      To clarify, the borrow checker is not disabled in unsafe blocks. Unsafe blocks just allow raw pointer dereferencing, which can be used to bypass the borrow checker.
kd5bjo 7y ago
> a demonstration that any program in the hypothetical dialect that can invoke undefined behaviour either uses `unsafe` or is rejected by the borrow checker. This isn’t quite what they’re doing here. They’re trying to define what guarantees the compiler should make about its treatment of unsafe code to strike a balance between usability and the ability of the compiler to optimize.
- mjw1007 7y ago
  Sure, but we want to be sure that the chosen model fits in correctly with the borrow checker. That's the part I was interested in.
  - kd5bjo 7y ago
    My apologies; I misread your original statement to imply that unsafe would necessarily imply undefined behavior.
jules 7y ago
The paper mentions that as future work: > In addition, we plan to connect Stacked Borrows with the formal Rust type system of RustBelt [Jung et al. 2018] to verify that in fact all safe Rust programs comply with Stacked Borrows.

zozbot234 7y ago

> Has the third been done, or is someone working on it? There has been a lot of work on this as part of the RustBelt project (that the OP is also a part of). But it's not "done" in any sense, for example traits are still unmodeled and a lot of the unsoundness of some kind or another that's been found in Rust has to do with them. The first goal is being worked on implicitly by the 'Rustonomicon' folks, who are trying to characterize "unsafe" Rust properly. Unsafe Rust is not "free of the borrow checker" in practice, but it's the part of the language that lets you do things which might be UB. So the two are obviously related.

viraptor 7y ago

> Has the third been done, or is someone working on it? Can this be done though? The way I understand this: Either 1. the whole model is specified and can be proven, (which wouldn't need the second step) or 2. you can only find specific counter-examples, not demonstrate there aren't any. (That would be like a solution to the halting problem) Did I miss something?

mjw1007 7y ago
If you're trying to analyse a program statically and find some property of its runtime behaviour, the halting problem only gets in the way when you need to be accurate about both whether the runtime behaviour does or doesn't have the property. Here, it's OK if the borrow checker rejects some programs which the stacked-borrows runtime model would say don't in fact invoke undefined behaviour, so long as it doesn't accept any which do. (And it surely will give some rejections of that sort, for example if I violate the borrowing rules in a function which is never called.)
- kd5bjo 7y ago
  Also, this is the primary reason that unsafe exists— there exists code that is both useful and correct but the borrow checker can’t properly verify. It’s a marker that tells the compiler it’s not responsible for verifying that code.
  - smaddox 7y ago
    To clarify, the borrow checker is not disabled in unsafe blocks. Unsafe blocks just allow raw pointer dereferencing, which can be used to bypass the borrow checker.

kd5bjo 7y ago

> a demonstration that any program in the hypothetical dialect that can invoke undefined behaviour either uses `unsafe` or is rejected by the borrow checker. This isn’t quite what they’re doing here. They’re trying to define what guarantees the compiler should make about its treatment of unsafe code to strike a balance between usability and the ability of the compiler to optimize.

mjw1007 7y ago
Sure, but we want to be sure that the chosen model fits in correctly with the borrow checker. That's the part I was interested in.
- kd5bjo 7y ago
  My apologies; I misread your original statement to imply that unsafe would necessarily imply undefined behavior.

jules 7y ago

The paper mentions that as future work: > In addition, we plan to connect Stacked Borrows with the formal Rust type system of RustBelt [Jung et al. 2018] to verify that in fact all safe Rust programs comply with Stacked Borrows.