Stacked Borrows: an aliasing model for Rust
ralfj.de
ralfj.de
One of the weakest areas of Rust (in some sense) is unsafe; we don't have a proper understanding of what exactly is acceptable with unsafe code. Projects like these are working on proposing a model for what those rules should be.
So, if you're most Rust programmers, this doesn't affect you, really, other than making code you depend on a bit higher quality :). If you're an author of unsafe Rust code, this would tell you what you can and can't do, and if you work on a compiler, these rules would tell you what you can and can't optimize.
Additionally, this is pretty neat:
> I hope to explore this question further in the following weeks by implementing a dynamic checker to test the model on real code.
If we accepted this model (which is, of course, a big if; it was just proposed!), then we could take this tool and instrument your unsafe, an "unsafegrind", if you will, that could tell you at runtime if your code trips UB.
This tooling is enabled by MIRI, which is also amazing, but I've gone on too long already. TL;DR: it's sort of a "rust interpreter" that we've invested in for compile-time function evaluation, but also pays off with things like this.
https://github.com/solson/miri is probably the best place to start poking around :)
An argument often made in favor of Rust's static analysis restrictions is that "worst case scenario, you just drop down to unsafe and you're back to C semantics".
However, this only holds true as long as the rules to uphold in unsafe code are easy to explain. Strict type aliasing in C is already considered as somewhat of a disaster by many, and is way simpler.
I hope they get this right.
The expressive problems with the ownership model mostly involve backpointers. It's hard to create doubly-linked lists or trees with backpointers in safe Rust, short of going to reference counts and weak pointers. This proposal doesn't seem to address that. Backlinks imply a consistency constraint between forward and back pointers, and Rust lacks the expressive power to talk about that.
The other big expressive issue involves partially initialized arrays. The underlying machinery for a vector involves getting uninitialized memory and initializing it one entry at a time as more of the vector's space is used. You can't talk about that within Rust. It's the sort of thing for which a simple inductive proof is needed, once you're able to say things like "Only elements 0..N of this array are valid".
These are places where you need unsafe Rust because you can't say what you mean in safe Rust. That's the first problem, insufficient expressive power. The second problem is proving that what you said is correct. That's a technical compiler/verifier issue.
Which it has been for too long. I was doing automated program proving on basic validity stuff like this over 30 years ago.
In order to prove something, you first need a notation for talking about it. Few languages let you talk about uninitialized memory space properly. Constructors are too magic.
Un-initialized memory can be viewed as write-only. You want to show that no un-initialized byte is ever read. Memory comes from the allocator in blocks of un-initialized bytes.
A constructor is simply a function that takes a block of un-initialized memory and assigns every byte to something meaningful for that type. At the end of construction, the memory block becomes a valid instance of that type.
Once you can talk about construction as a non-magic operation, you can talk about partial construction of an array. Until you can talk about it, you can't prove anything about it.
Some types, such as "byte", are fully mapped - any bit pattern is valid. So they can be initialized by anything that fills them. That's how input buffers can be expressed.
In C++, the constructor doesn't initialise every bytes (padding for example)..
It's true that it's dynamic construction (although other similar constructs allow for doing it for statically sized arrays), but it is demonstrating Rust's power: making safe APIs over `unsafe` code without having to delve into the depths of a complicated compiler/proof-assistant. This is exactly what `unsafe` is for: extending what safe code can do by temporarily stepping outside the bounds of what the language directly encodes.
I don't see how baking special cases for safety into the compiler is any better than having more general tooling, and constructing safe wrappers in Rust.
Also, just for some context, you're often complaining that Rust is too complicated comparing it to C++. Your desires for extra power to reason about pointer-soups (or writing inductive proofs in the language, rather than using existing tooling for it) aren't going to fix that at all, and indeed are likely to add a whole extra level of complexity.
It doesn't seem like a good use of time, or "language-complexity budget", to have the language features that specifically allow `Vec<T>` to be implemented safely, when that can all just be done in (not-that-complicated) normal Rust code. Additionally, reasoning about code (i.e. feeling satisfied in its correctness) is almost always easier than reasoning about code that reasons about code (i.e. feeling satisfied that the proof-checker/compile will correctly prove other code's correctness).
Plenty of pure Rust code uses pointers. They're necessary for the implementation of things like `Vec`. Raw pointers aren't going anywhere.
> The expressive problems with the ownership model mostly involve backpointers.
These problems can be trivially solved in 95% of cases with arena allocation. The other 5% fundamentally require bespoke solutions because you're trying to do something elaborate/niche.
More importantly, the lack of soundness guarantees in unsafe Rust is a more critical problem. This is because unsafe is the primary mechanism to supplement safe Rust when safe Rust isn't expressive enough – it's not just for FFI like you claim! That foundation needs to be rock solid, and this work is addressing that problem.
Btw. backpointers require a guarantee that the values pointed at are not moved as long as the pointers themselves are valid. Before, the compiler would ensure that things borrowed from didn't move, but that isn't enough to implement some systems with longer-living or self-referential pointers. And generally Rust doesn't guarantee that things won't move around. But there is going to be support for "pinning" values. That still doesn't get you all you need for backpointers (which have really complicated semantics if you think about it!), but again, one step of expressivity more that allows you to implement backpointers in unsafe code, but then expose a safe interface where you can get "pinned" references to the nodes.
That's what I'm getting at here. There are only a few special cases where you really need unsafe code. Backpointers, partially initialized arrays, and foreign functions cover most of it. Yes, you can construct fancy situations like hash maps where there's some performance benefit in having complicated sparse arrays of pointers interspersed with junk. Is it worth it? Zeroing memory is cheap. Go zeros everything and doesn't seem to suffer.
The use case of Rust is memory safety without garbage collection. Keep that in mind. Try not to get too clever. Too much "unsafe", and it will break. Not just through coding bugs. Because someone will change something that was based on an implicit assumption made in the past by another.
> Go zeros everything and doesn't seem to suffer.
What are you referring to by this? For most CPU bound things, Go is measurably slower than Rust. If you mean that Go is successful as a language, well... that's almost like saying "why do you need structs/value types? Python allocates everything and doesn't seem to suffer". The languages have different domains/primary targets.
It was a really amazing read.