# Stacked Borrows Implemented **URL:** \ **Category:** Unsafe Code Guidelines\ **Created:** [November 16, 2018, 4:54pm UTC](https://internals.rust-lang.org/t/stacked-borrows-implemented/8847 "2018-11-16T16:54:42Z")\ **Posts on this page:** 17\ **Page:** 1
**Author:** ![RalfJung](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/ralfjung/32/2415_2.png) [@RalfJung](https://internals.rust-lang.org/u/RalfJung)\ **Post date:** [November 16, 2018, 4:54pm UTC](https://internals.rust-lang.org/t/stacked-borrows-implemented/8847/1 "2018-11-16T16:54:42Z")
Three months ago, I proposed _Stacked Borrows_ as a model for defining what kinds of aliasing are allowed in Rust, and the idea of a _validity invariant_ that has to be maintained by all code at all times. Since then I have been busy implementing both of these, and developed Stacked Borrows further in doing so. This post describes the latest version of Stacked Borrows, and reports my findings from the implementation phase: What worked, what did not, and what remains to be done. There will also be an opportunity for you to help the effort! [https://www.ralfj.de/blog/2018/11/16/stacked-borrows-implementation.html](https://www.ralfj.de/blog/2018/11/16/stacked-borrows-implementation.html) ---
**Author:** ![RalfJung](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/ralfjung/32/2415_2.png) [@RalfJung](https://internals.rust-lang.org/u/RalfJung)\ **Post date:** [November 19, 2018, 2:41pm UTC](https://internals.rust-lang.org/t/stacked-borrows-implemented/8847/2 "2018-11-19T14:41:39Z")
In case you are familiar with `async fn`/futures, here’s another issue where you could help 😃 > ---
**Author:** ![gnzlbg](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/gnzlbg/32/3858_2.png) [@gnzlbg](https://internals.rust-lang.org/u/gnzlbg)\ **Post date:** [November 20, 2018, 8:10am UTC](https://internals.rust-lang.org/t/stacked-borrows-implemented/8847/3 "2018-11-20T08:10:36Z")
> Secondly, _reading_ through a mutable reference is actually okay _even when that reference is not exclusive_ . Does LLVM `noalias` affect optimizations only when reading through pointers? For example, if I have a `&mut` and a `&`, and I cast them to raw pointers and compare them for equality, I'd expect the comparison to be optimized away if the `&mut` is `noalias` because no other pointer in the current scope can alias that memory, and therefore, cannot be pointing to that memory. So two such pointers cannot be equal. But maybe my logic is flawed. ---
**Author:** ![RalfJung](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/ralfjung/32/2415_2.png) [@RalfJung](https://internals.rust-lang.org/u/RalfJung)\ **Post date:** [November 21, 2018, 9:14am UTC](https://internals.rust-lang.org/t/stacked-borrows-implemented/8847/4 "2018-11-21T09:14:27Z")
I made a [small update](https://git.ralfj.de/web.git/history/refs/heads/master:/ralf/_posts/2018-11-16-stacked-borrows-implementation.md): Dereferencing a pointer now always preserves the tag, but casting to a raw pointer resets the tag to `Shr(None)` . `Box` is treated like a mutable reference. * * * > [@gnzlbg](#): > > Does LLVM `noalias` affect optimizations only when reading through pointers? No, it basically says operations on this pointer do not conflict with operations on other pointers. Since two reads never conflict, that gives a little more freedom for reads. > [@gnzlbg](#): > > I’d expect the comparison to be optimized away `noalias` says nothing about whether the pointers are equal, and cannot be used for optimizing equality tests. For example, in the following function, both arguments are marked noalias, yet clearly the pointers could be equal: ```rust fn foo(x: &i32, y: &i32) -> bool { x as *const _ == y as *const _ } ``` ---
**Author:** ![felix91gr](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/felix91gr/32/4380_2.png) [@felix91gr](https://internals.rust-lang.org/u/felix91gr)\ **Post date:** [November 21, 2018, 10:46pm UTC](https://internals.rust-lang.org/t/stacked-borrows-implemented/8847/5 "2018-11-21T22:46:52Z")
> [@RalfJung](#): > > Three months ago, I proposed _Stacked Borrows_ as a model for defining what kinds of aliasing are allowed in Rust, and the idea of a _validity invariant_ that has to be maintained by all code at all times Sorry if I'm asking something that's maybe too obvious. What's the idea of developing this model? Is it to prove correctness of the Rust borrow checker, or is the idea to construct a more ergonomic one? Maybe the idea is to provide an example correct-by-construction implementation of it? What is it? I'm really curious 🙂 PS: for how little I know of memory management and aliasing, your post is quite readable. Thanks for taking the time to make it so! 😊 ---
**Author:** ![Ixrec](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/ixrec/32/6754_2.png) [@Ixrec](https://internals.rust-lang.org/u/Ixrec)\ **Post date:** [November 21, 2018, 11:19pm UTC](https://internals.rust-lang.org/t/stacked-borrows-implemented/8847/6 "2018-11-21T23:19:32Z")
I’m not directly involved in any of these efforts, but to check my own understanding… The primary motivation is that Rust currently has no formal specification to tell us what is and isn’t legal `unsafe` code, i.e. what `unsafe` code triggers UB (undefined behavior) and what doesn’t. That’s a pretty big deal for all `unsafe` code in the ecosystem, and all the safe code that relies on it (which amounts to all Rust code ever). It’s arguably the only sense in which Rust is “less safe” than C++ today; in Rust it’s not even possible to know if your `unsafe` code is UB or not. So if “Stacked Borrows” turns out to be a good fit for all unsafe Rust code in the wild, we might have an RFC to formally adopt it as (a big part of) the official definition of UB in Rust. A very close second motivation is that it seems like we can do way better than just adopting a formal spec. First, mere mortals like you and me can actually understand this model! (I still don’t have a clue whether any of my C++ code is technically UB) Second, even the compiler understands it, so it can programmatically verify the presence of absence of UB! There’s probably a ton of caveats on that (we obviously can’t check FFI, unlike the borrow checker you need very thorough test coverage, etc), but that would still be amazing. ---
**Author:** ![felix91gr](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/felix91gr/32/4380_2.png) [@felix91gr](https://internals.rust-lang.org/u/felix91gr)\ **Post date:** [November 21, 2018, 11:25pm UTC](https://internals.rust-lang.org/t/stacked-borrows-implemented/8847/7 "2018-11-21T23:25:18Z")
Wow, wow, that’s amazing! So, it’s like the sibling of the borrow checker, the difference being that this one checks the safety (or non-UB quality of, at least) of `unsafe` code 😃 ---
**Author:** ![RalfJung](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/ralfjung/32/2415_2.png) [@RalfJung](https://internals.rust-lang.org/u/RalfJung)\ **Post date:** [November 22, 2018, 10:40am UTC](https://internals.rust-lang.org/t/stacked-borrows-implemented/8847/8 "2018-11-22T10:40:35Z")
@Ixrec Well put. 🙂 Just one minor thing: > [@Ixrec](#): > > Second, even the compiler understands it, so it can programmatically verify the presence of absence of UB! The compiler doesn't really, miri does, which is an interpreter based on the compiler. Think of it like one of these sanitizers (msan, asan etc) that exist for C/C++ code. > [@felix91gr](#): > > So, it’s like the sibling of the borrow checker, the difference being that this one checks the safety (or non-UB quality of, at least) of `unsafe` code 😃 Kind-of, yes, but there is one more very important difference: The borrow checker is _static_: you run it once on a piece of code, and you know that all ways of executing that code in any way (with any possible values for the arguments etc.) are safe. Stacked Borrows and its implementation in miri are _dynamic_: you can run your code with it, given concrete inputs and concrete values for all variables, and then it tells you whether your code is safe. To get the same guarantee as the static check (safety for all possible inputs), you would have to try all possible inputs, of which there are way too many. So the guarantee you get is weaker, but then on the plus side you can also use it for `unsafe` code. Basically, for Stacked Borrows and miri to be useful, you better have a good test suite with excellent coverage. And even then you cannot be sure what happens when you try other inputs. The borrow checker doesn't need any test suite, it can handle all inputs at once -- but it only works on safe code. ---
**Author:** ![felix91gr](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/felix91gr/32/4380_2.png) [@felix91gr](https://internals.rust-lang.org/u/felix91gr)\ **Post date:** [November 22, 2018, 12:06pm UTC](https://internals.rust-lang.org/t/stacked-borrows-implemented/8847/9 "2018-11-22T12:06:02Z")
> [@RalfJung](#): > > Think of it like one of these sanitizers (msan, asan etc) that exist for C/C++ code. Ohh, I get it now. A testing suite that runs miri with the Stacked Borrows system sounds like a really good idea! 😃 > [@RalfJung](#): > > The borrow checker doesn’t need any test suite, it can handle all inputs at once That reminds me of universal quantifiers in 1st-order logic (this would be the borrow checker) v/s propositional logic (this would be the stacked borrows system). Do both systems share a relationship like that one? Can one be expressed in terms of the other, in some sense? ---
**Author:** ![skippy](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/skippy/32/5542_2.png) [@skippy](https://internals.rust-lang.org/u/skippy)\ **Post date:** [November 22, 2018, 1:06pm UTC](https://internals.rust-lang.org/t/stacked-borrows-implemented/8847/10 "2018-11-22T13:06:40Z")
> [@RalfJung](#): > > The compiler doesn't really, miri does, which is an interpreter based on the compiler. Think of it like one of these sanitizers (msan, asan etc) that exist for C/C++ code. From what I understand, the sanitizers you mention aren't interpreted and run as compiled, instrumented code. Could a sanitizer theoretically implement the stacked borrows model in a fully compiled, but instrumented, Rust program? I'm not sure if this would buy anything. ---
**Author:** ![RalfJung](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/ralfjung/32/2415_2.png) [@RalfJung](https://internals.rust-lang.org/u/RalfJung)\ **Post date:** [November 22, 2018, 1:23pm UTC](https://internals.rust-lang.org/t/stacked-borrows-implemented/8847/11 "2018-11-22T13:23:56Z")
> [@felix91gr](#): > > That reminds me of universal quantifiers in 1st-order logic (this would be the borrow checker) v/s propositional logic (this would be the stacked borrows system). Do both systems share a relationship like that one? Can one be expressed in terms of the other, in some sense? It's about a universal quantification, yes -- the borrow checker checks "is this safe _for all inputs_, Stacked Borrows checks (defines, really) "is this safe _for one particular given input_". There is also a difference in precision though: The borrow checker will sometimes reject code that is actually safe for all inputs, because code can be too complicated for an automated check to figure out that it is always safe. That is the case for all the unsafe code wrapped in safe abstractions, actually (except for the ones that have bugs 😉 ). > [@skippy](#): > > From what I understand, the sanitizers you mention aren’t interpreted and run as compiled, instrumented code. Could a sanitizer theoretically implement the stacked borrows model in a fully compiled, but instrumented, Rust program? I’m not sure if this would buy anything. The only difference between interpretation and instrumented machine-code execution is the speed at which it runs. So yes, Stacked Borrows could also be implemented as instrumented compilation, and that would (a) be much faster than miri, and (b) allow FFI to C. It would however probably also be less precise, probably. ---
**Author:** ![ange](https://avatars.discourse-cdn.com/v4/letter/a/76d3ee/32.png) [@ange](https://internals.rust-lang.org/u/ange)\ **Post date:** [December 9, 2018, 8:30am UTC](https://internals.rust-lang.org/t/stacked-borrows-implemented/8847/12 "2018-12-09T08:30:14Z")
> [@RalfJung](#): > > It's about a universal quantification, yes -- the borrow checker checks "is this safe _for all inputs_, Stacked Borrows checks (defines, really) "is this safe _for one particular given input_". I'm not entirely clear on which bits of unsafe code you're targeting here. One question that springs to mind is: for relatively self-contained code, would it not be possible to go from "safe for a particular input" to "safe for all inputs" by [symbolically executing](https://arxiv.org/pdf/1610.00502.pdf) the unsafe code (including the stacked borrows instrumentation) starting from memory and registers that are all symbolic? AFAIU, this should work for unsafe code that does statically bounded pointer-chasing (though perhaps that's not interesting?). Alternatively, (heap) shape analysis or significantly bounding the size of the symbolic memory (neither of which may be simple, of course) might help? Though again, don't have any concrete examples of the type of code that you'd want to check. ---
**Author:** ![RalfJung](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/ralfjung/32/2415_2.png) [@RalfJung](https://internals.rust-lang.org/u/RalfJung)\ **Post date:** [December 9, 2018, 4:54pm UTC](https://internals.rust-lang.org/t/stacked-borrows-implemented/8847/13 "2018-12-09T16:54:32Z")
> [@ange](#): > > would it not be possible to go from “safe for a particular input” to “safe for all inputs” by [symbolically executing](https://arxiv.org/pdf/1610.00502.pdf) the unsafe code (including the stacked borrows instrumentation) starting from memory and registers that are all symbolic? Sure, that is always the case. Once you have a definition "safe for some input", you can define "for all inputs, safe for that input", and you can try to prove that for some particular function. This will not always be possible automatically, but symbolic execution is one of many techniques that one could try to use and it will work in some cases. Once we have a better understanding of Stacked Borrows, I certainly hope such tools will be developed! (I have no experience with symbolic execution myself.) ---
**Author:** ![felix91gr](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/felix91gr/32/4380_2.png) [@felix91gr](https://internals.rust-lang.org/u/felix91gr)\ **Post date:** [December 9, 2018, 8:13pm UTC](https://internals.rust-lang.org/t/stacked-borrows-implemented/8847/14 "2018-12-09T20:13:17Z")
I love that this is being discussed. @ange, @RalfJung you guys are awesome 🙌🏻 ---
**Author:** ![ange](https://avatars.discourse-cdn.com/v4/letter/a/76d3ee/32.png) [@ange](https://internals.rust-lang.org/u/ange)\ **Post date:** [December 10, 2018, 6:44pm UTC](https://internals.rust-lang.org/t/stacked-borrows-implemented/8847/15 "2018-12-10T18:44:50Z")
> [@RalfJung](#): > > Sure, that is always the case. Once you have a definition "safe for some input", you can define "for all inputs, safe for that input", and you can try to prove that for some particular function. This will not always be possible automatically, but symbolic execution is one of many techniques that one could try to use and it will work in some cases. Once we have a better understanding of Stacked Borrows, I certainly hope such tools will be developed! (I have no experience with symbolic execution myself.) That's great to hear. I only have (limited) experience with symbolic execution. Which of those other techniques would you consider semi-practical for this task? ---
**Author:** ![RalfJung](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/ralfjung/32/2415_2.png) [@RalfJung](https://internals.rust-lang.org/u/RalfJung)\ **Post date:** [December 10, 2018, 10:13pm UTC](https://internals.rust-lang.org/t/stacked-borrows-implemented/8847/16 "2018-12-10T22:13:51Z")
I’d say we should throw everything we have at it. 😃 I am not an expert in automated analysis. Another approach might be abstract interpretation, or some kind of automated theorem proving, and then there are approaches that need some help from the user (which might be reasonable for critical code). Really, you could occupy an entire swarm of grad students with projects to throw all verification methods known to man at this problem. 😛 The main challenge remains developing something that actually works on real-world code and can be meaningfully embedded into productive development (as opposed to a one-off verification effort that becomes meaningless with the next refactoring). ---
**Author:** ![system](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/system/32/14092_2.png) [@system](https://internals.rust-lang.org/u/system)\ **Post date:** [March 25, 2019, 8:31am UTC](https://internals.rust-lang.org/t/stacked-borrows-implemented/8847/17 "2019-03-25T08:31:10Z")
Closed on March 25, 2019, 8:31am UTC This topic was automatically closed 90 days after the last reply. New replies are no longer allowed.