Stacked Borrows: An Aliasing Model for Rust
plv.mpi-sws.org
plv.mpi-sws.org
- 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?
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.
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?
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.)
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.
> 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.
That's the wrong mental model. The compiler doesn't decide to treat some code as "undefined". Instead, the compiler assumes all code is not "undefined", and generates code according to that. The compiler might notice that the code is doing bad things, and warn the developer (or even return an error), but that's not guaranteed, since undefined behavior is generally things the compiler cannot easily check.
For an example, Rust guarantees that no two mutable references can reference the same place at the same time, even in unsafe code. If a function receives a pair of mutable references, the compiler assumes that they do not overlap. If they in fact overlap, the code generated by the compiler might do the wrong thing.
https://gcc.gnu.org/ml/gcc/2016-02/msg00381.html
"The fact is, undefined compiler behavior is never a good idea. Not for serious projects.
Performance doesn't come from occasional small and odd micro-optimizations. I care about performance a lot, and I actually look at generated code and do profiling etc. None of those three options have ever shown up as issues. But the incorrect code they generate? It has."
This paper isn't about that (nor is it necessarily about unsafe Rust). It's about compiler optimisations. Because Rust has very clear rules about references and borrows, the idea is to come up with a model for Rust code that allows for a particular optimisation (namely, to allow telling the compiler that two pointers do not alias -- do not refer to the same memory). Obviously unsafe code would need to make sure it obeys this new memory model, otherwise the code would be invoking undefined behaviour.
In safe rust, the compiler gives a mathematical proof this is so. In unsafe code, the compiler does not, but still assumes these properties are holding. The burden to make sure everything is correct falls on the shoulders of the programmers.
But nobody knows exactly what these properties are. There is a big part known, but the edges are fuzzy. So unsafe code is required to follow rules nobody knows.
This effort is part of the work to clarify the rules. If accepted, both the compiler and unsafe programmer knows how far they are allowed to go
What it is, is a formal specification for something like an UB Sanitizer.