X-Git-Url: https://git.ralfj.de/web.git/blobdiff_plain/81016b7c2a9987023f97d12f4281108012785aab..refs/heads/master:/ralf/_posts/2018-11-16-stacked-borrows-implementation.md diff --git a/ralf/_posts/2018-11-16-stacked-borrows-implementation.md b/ralf/_posts/2018-11-16-stacked-borrows-implementation.md deleted file mode 100644 index 211d21d..0000000 --- a/ralf/_posts/2018-11-16-stacked-borrows-implementation.md +++ /dev/null @@ -1,911 +0,0 @@ ---- -title: "Stacked Borrows Implemented" -categories: internship rust ---- - -Three months ago, I proposed [Stacked Borrows]({% post_url -2018-08-07-stacked-borrows %}) as a model for defining what kinds of aliasing -are allowed in Rust, and the idea of a [validity invariant]({% post_url -2018-08-22-two-kinds-of-invariants %}) 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! - - - -What Stacked Borrows does is that it defines a semantics for Rust programs such -that some things about references always hold true for every valid execution -(meaning executions where no [undefined behavior]({% post_url -2017-07-14-undefined-behavior %}) occurred): `&mut` references are unique (we -can rely on no accesses by other functions happening to the memory they point -to), and `&` references are immutable (we can rely on no writes happening to the -memory they point to, unless there is an `UnsafeCell`). Usually we have the -borrow checker guarding us against such nefarious violations of reference type -guarantees, but alas, when we are writing unsafe code, the borrow checker cannot -help us. We have to define a set of rules that makes sense even for unsafe -code. - -I will explain these rules again in this post. The explanation is not going to -be the same as last time, not only because it changed a bit, but also because I -think I understand the model better myself now so I can do a better job -explaining it. - -Ready? Let's get started. I hope you brought some time, because this is a -rather lengthy post. If you are not interested in a detailed description of -Stacked Borrows, you can skip most of this post and go right to [section 4]. If -you only want to know how to help, jump to [section 6]. - -## 1 Enforcing Uniqueness - -Let us first ignore the part about `&` references being immutable and focus on -uniqueness of mutable references. Namely, we want to define our model in a way -that calling the following function will trigger undefined behavior: - -{% highlight rust %} -fn demo0() { - let x = &mut 1u8; - let y = &mut *x; - *y = 5; - // Write through a pointer aliasing `y` - *x = 3; - // Use `y` again, asserting it is still exclusive - let _val = *y; -} -{% endhighlight %} - -We want this function to be disallowed because between two uses of `y`, there is -a use of another pointer for the same location, violating the fact that `y` -should be unique. - -Notice that this function does not compile, the borrow checker won't allow it. -That's great! It is undefined behavior, after all. But the entire point of -this exercise is to explain *why* we have undefined behavior here *without* -referring to the borrow checker, because we want to have rules that also work -for unsafe code. In fact, you could say that retroactively, these rules explain -why the borrow checker works the way it does: We can pretend that the model came -first, and the borrow checker is merely doing compile-time checks to make sure -we follow the rules of the model. - -To be able to do this, we have to pretend our machine has two things which real -CPUs do not have. This is an example of adding "shadow state" or "instrumented -state" to the "virtual machine" that we [use to specify Rust]({% post_url -2017-06-06-MIR-semantics %}). This is not an uncommon approach, often times -source languages make distinctions that do not appear in the actual hardware. A -related example is -[valgrind's memcheck](http://valgrind.org/docs/manual/mc-manual.html) which -keeps track of which memory is initialized to be able to detect memory errors: -During a normal execution, uninitialized memory looks just like all other -memory, but to figure out whether the program is violating C's memory rules, we -have to keep track of some extra state. - -For stacked borrows, the extra state looks as follows: - -1. For every pointer, we keep track of an extra "tag" that records when and how - this pointer was created. -2. For every location in memory, we keep track of a stack of "items", indicating - which tag a pointer must have to be allowed to access this location. - -These exist separately, i.e., when a pointer is stored in memory, then we both -have a tag stored as part of this pointer value (remember, -[bytes are more than `u8`]({% post_url 2018-07-24-pointers-and-bytes %})), and -every byte occupied by the pointer has a stack regulating access to this -location. Also these two do not interact, i.e., when loading a pointer from -memory, we just load the tag that was stored as part of this pointer. The stack -of a location, and the tag of a pointer stored at some location, do not have any -effect on each other. - -In our example, there are two pointers (`x` and `y`) and one location of -interest (the one both of these pointers point to, initialized with `1u8`). -When we initially create `x`, it gets tagged `Uniq(0)` to indicate that it is a -unique reference, and the location's stack has `Uniq(0)` at its top to indicate -that this is the latest reference allowed to access said location. When we -create `y`, it gets a new tag, `Uniq(1)`, so that we can distinguish it from -`x`. We also push `Uniq(1)` onto the stack, indicating not only that `Uniq(1)` -is the latest reference allow to access, but also that it is "derived from" -`Uniq(0)`: The tags higher up in the stack are descendants of the ones further -down. - -So after both references are created, we have: `x` tagged `Uniq(0)`, `y` tagged -`Uniq(1)`, and the stack contains `[Uniq(0), Uniq(1)]`. (Top of the stack is on -the right.) - -When we use `y` to access the location, we make sure its tag is at the top of -the stack: check, no problem here. When we use `x`, we do the same thing: Since -it is not at the top yet, we pop the stack until it is, which is easy. Now the -stack is just `[Uniq(0)]`. Now we use `y` again and... blast! Its tag is not -on the stack. We have undefined behavior. - -In case you got lost, here is the source code with comments indicating the tags -and the stack of the one location that interests us: - -{% highlight rust %} -fn demo0() { - let x = &mut 1u8; // tag: `Uniq(0)` - // stack: [Uniq(0)] - - let y = &mut *x; // tag: `Uniq(1)` - // stack: [Uniq(0), Uniq(1)] - - // Pop until `Uniq(1)`, the tag of `y`, is on top of the stack: - // Nothing changes. - *y = 5; - // stack: [Uniq(0), Uniq(1)] - - // Pop until `Uniq(0)`, the tag of `x`, is on top of the stack: - // We pop `Uniq(1)`. - *x = 3; - // stack: [Uniq(0)] - - // Pop until `Uniq(1)`, the tag of `y`, is on top of the stack: - // That is not possible, hence we have undefined behavior. - let _val = *y; -} -{% endhighlight %} - -Well, actually having undefined behavior here is good news, since that's what we -wanted from the start! And since there is an implementation of the model in -[miri](https://github.com/solson/miri/), you can try this yourself: The amazing -@shepmaster has integrated miri into the playground, so you can -[put the example there](https://play.rust-lang.org/?version=stable&mode=debug&edition=2015&gist=d15868687f79072688a0d0dd1e053721) -(adjusting it slightly to circumvent the borrow checker), then select "Tools - -Miri" and it will complain (together with a rather unreadable backtrace, we sure -have to improve that one): - -``` -error[E0080]: constant evaluation error: Borrow being dereferenced (Uniq(1037)) does not exist on the stack - --> src/main.rs:6:14 - | -6 | let _val = *y; - | ^^ Borrow being dereferenced (Uniq(1037)) does not exist on the stack - | -``` - -## 2 Enabling Sharing - -If we just had unique pointers, Rust would be a rather dull language. Luckily -enough, there are also two ways to have shared access to a location: through -shared references (safely), and through raw pointers (unsafely). Moreover, -shared references *sometimes* (but not when they point to an `UnsafeCell`) -assert an additional guarantee: Their destination is immutable. - -For example, we want the following code to be allowed -- not least because this -is actually safe code accepted by the borrow checker, so we better make sure -this is not undefined behavior: - -{% highlight rust %} -fn demo1() { - let x = &mut 1u8; - // Create several shared references, and we can also still read from `x` - let y1 = &*x; - let _val = *x; - let y2 = &*x; - let _val = *y1; - let _val = *y2; -} -{% endhighlight %} - -However, the following code is *not* okay: - -{% highlight rust %} -fn demo2() { - let x = &mut 1u8; - let y = &*x; - // Create raw reference aliasing `y` and write through it - let z = x as *const u8 as *mut u8; - unsafe { *z = 3; } - // Use `y` again, asserting it still points to the same value - let _val = *y; -} -{% endhighlight %} - -If you -[try this in miri](https://play.rust-lang.org/?version=stable&mode=debug&edition=2015&gist=1bc8c2f432941d02246fea0808e2e4f4), -you will see it complain: - -``` - --> src/main.rs:6:14 - | -6 | let _val = *y; - | ^^ Location is not frozen long enough - | -``` - -How is it doing that, and what is a "frozen" location? - -To explain this, we have to extend the "shadow state" of our "virtual machine" a -bit. First of all, we introduce a new kind of tag that a pointer can carry: A -*shared* tag. The following Rust type describes the possible tags of a pointer: - -{% highlight rust %} -pub type Timestamp = u64; -pub enum Borrow { - Uniq(Timestamp), - Shr(Option), -} -{% endhighlight %} - -You can think of the timestamp as a unique ID, but as we will see, for shared -references, it is also important to be able to determine which of these IDs was -created first. The timestamp is optional in the shared tag because that tag is -also used by raw pointers, and for raw pointers, we are often not able to track -when and how they are created (for example, when raw pointers are converted to -integers and back). - -We use a separate type for the items on our stack, because there we do not need -a timestamp for shared pointers: - -{% highlight rust %} -pub enum BorStackItem { - Uniq(Timestamp), - Shr, -} -{% endhighlight %} - -And finally, a "borrow stack" consists of a stack of `BorStackItem`, together -with an indication of whether the stack (and the location it governs) is -currently *frozen*, meaning it may only be read, not written: - -{% highlight rust %} -pub struct Stack { - borrows: Vec, // used as a stack; never empty - frozen_since: Option, // virtual frozen "item" on top of the stack -} -{% endhighlight %} - -### 2.1 Executing the Examples - -Let us now look at what happens when we execute our two example programs. To -this end, I will embed comments in the source code. There is only one location -of interest here, so whenever I talk about a "stack", I am referring to the -stack of that location. - -{% highlight rust %} -fn demo1() { - let x = &mut 1u8; // tag: `Uniq(0)` - // stack: [Uniq(0)]; not frozen - - let y1 = &*x; // tag: `Shr(Some(1))` - // stack: [Uniq(0), Shr]; frozen since 1 - - // Access through `x`. We first check whether its tag `Uniq(0)` is in the - // stack (it is). Next, we make sure that either our item *or* `Shr` is on - // top *or* the location is frozen. The latter is the case, so we go on. - let _val = *x; - // stack: [Uniq(0), Shr]; frozen since 1 - - // This is not an access, but we still dereference `x`, so we do the same - // actions as on a read. Just like in the previous line, nothing happens. - let y2 = &*x; // tag: `Shr(Some(2))` - // stack: [Uniq(0), Shr]; frozen since 1 - - // Access through `y1`. Since the shared tag has a timestamp (1) and the type - // (`u8`) does not allow interior mutability (no `UnsafeCell`), we check that - // the location is frozen since (at least) that timestamp. It is. - let _val = *y1; - // stack: [Uniq(0), Shr]; frozen since 1 - - // Same as with `y2`: The location is frozen at least since 2 (actually, it - // is frozen since 1), so we are good. - let _val = *y2; - // stack: [Uniq(0), Shr]; frozen since 1 -} -{% endhighlight %} - -This example demonstrates a few new aspects. First of all, there are actually -two operations that perform tag-related checks in this model (so far): -Dereferencing a pointer (whenever you have a `*`, also implicitly), and actual -memory accesses. Operations like `&*x` are an example of operations that -dereference a pointer without accessing memory. Secondly, *reading* through a -mutable reference is actually okay *even when that reference is not exclusive*. -It is only *writing* through a mutable reference that "re-asserts" its -exclusivity. I will come back to these points later, but let us first go -through another example. - -{% highlight rust %} -fn demo2() { - let x = &mut 1u8; // tag: `Uniq(0)` - // stack: [Uniq(0)]; not frozen - - let y = &*x; // tag: `Shr(Some(1))` - // stack: [Uniq(0), Shr]; frozen since 1 - - // The `x` here really is a `&*x`, but we have already seen above what - // happens: `Uniq(0)` must be in the stack, but we leave it unchanged. - let z = x as *const u8 as *mut u8; // tag irrelevant because raw - // stack: [Uniq(0), Shr]; frozen since 1 - - // A write access through a raw pointer: Unfreeze the location and make sure - // that `Shr` is at the top of the stack. - unsafe { *z = 3; } - // stack: [Uniq(0), Shr]; not frozen - - // Access through `y`. There is a timestamp in the `Shr` tag, and the type - // `u8` does not allow interior mutability, but the location is not frozen. - // This is undefined behavior. - let _val = *y; -} -{% endhighlight %} - -### 2.2 Dereferencing a Pointer -[section 2.2]: #22-dereferencing-a-pointer - -As we have seen, we consider the tag of a pointer already when dereferencing it, -before any memory access happens. The operation on a dereference never mutates -the stack, but it performs some basic checks that might declare the program UB. -The reason for this is twofold: First of all, I think we should require some -basic validity for pointers that are dereferenced even when they do not access -memory. Secondly, there is the practical concern for the implementation in miri: -When we dereference a pointer, we are guaranteed to have type information -available (crucial for things that depend on the presence of an `UnsafeCell`), -whereas having type information on every memory access would be quite hard to -achieve in miri. - -Notice that on a dereference, we have *both* a tag at the pointer *and* the type -of a pointer, and the two might not agree, which we do not always want to rule -out (after a `transmute`, we might have raw or shared pointers with a unique -tag, for example). - -The following checks are done on every pointer dereference, for every location -covered by the pointer (`size_of_val` tells us how many bytes the pointer -covers): - -1. If this is a raw pointer, do nothing and reset the tag used for the access to - `Shr(None)`. Raw accesses are checked as little as possible. -2. If this is a unique reference and the tag is `Shr(Some(_))`, that's an error. -3. If the tag is `Uniq`, make sure there is a matching `Uniq` item with the same - ID on the stack. -4. If the tag is `Shr(None)`, make sure that either the location is frozen or - else there is a `Shr` item on the stack. -5. If the tag is `Shr(Some(t))`, then the check depends on whether the location - is inside an `UnsafeCell` or not, according to the type of the reference. - - Locations outside `UnsafeCell` must have `frozen_since` set to `t` or an - older timestamp. - - `UnsafeCell` locations must either be frozen or else have a `Shr` item in - their stack (same check as if the tag had no timestamp). - -### 2.3 Accessing Memory -[section 2.3]: #23-accessing-memory - -On an actual memory access, we know the tag of the pointer that was used to -access (unless it was a raw pointer, in which case the tag we see is -`Shr(None)`), and we know whether we are reading from or writing to the current -location. We perform the following operations on all locations affected by the -access: - -1. If the location is frozen and this is a read access, nothing happens (even - if the tag is `Uniq`). -2. Unfreeze the location (set `frozen_since` to `None`). Either the location is - already unfrozen, or this is a write. -3. Pop the stack until the top item matches the tag of the pointer. - - A `Uniq` item matches a `Uniq` tag with the same ID. - - A `Shr` item matches any `Shr` tag (with or without timestamp). - - When we are reading, a `Shr` item matches a `Uniq` tag. - - If we pop the entire stack without finding a match, then we have undefined - behavior. - -To understand these rules better, try going back through the three examples we -have seen so far and applying these rules for dereferencing pointers and -accessing memory to understand how they interact. - -The most subtle point here is that we make a `Uniq` tag match a `Shr` item and -also accept `Uniq` reads on frozen locations. This is required to make `demo1` -work: Rust permits read accesses through mutable references even when they are -not currently actually unique. Our model hence has to do the same. - -## 3 Retagging and Creating Raw Pointers - -We have talked quite a bit about what happens when we *use* a pointer. It is -time we take a close look at *how pointers are created*. However, before we go -there, I would like us to consider one more example: - -{% highlight rust %} -fn demo3(x: &mut u8) -> u8 { - some_function(); - *x -} -{% endhighlight %} - -The question is: Can we move the load of `x` to before the function call? -Remember that the entire point of Stacked Borrows is to enforce a certain -discipline when using references, in particular, to enforce uniqueness of -mutable references. So we should hope that the answer to that question is "yes" -(and that, in turn, is good because we might use it for optimizations). -Unfortunately, things are not so easy. - -The uniqueness of mutable references entirely rests on the fact that the pointer -has a unique tag: If our tag is at the top of the stack (and the location is not -frozen), then any access with another tag will pop our item from the stack (or -cause undefined behavior). This is ensured by the memory access checks. Hence, -if our tag is *still* on the stack after some other accesses happened (and we -know it is still on the stack every time we dereference the pointer, as per the -dereference checks described above), we know that no access through a pointer -with a different tag can have happened. - -### 3.1 Guaranteed Freshness - -However, what if `some_function` has an exact copy of `x`? We got `x` from our -caller (whom we do not trust), maybe they used that same tag for another -reference (copied it with `transmute_copy` or so) and gave that to -`some_function`? There is a simple way we can circumvent this concern: Generate -a new tag for `x`. If *we* generate the tag (and we know generation never emits -the same tag twice, which is easy), we can be sure this tag is not used for any -other reference. So let us make this explicit by putting a `Retag` instruction -into the code where we generate new tags: - -{% highlight rust %} -fn demo3(x: &mut u8) -> u8 { - Retag(x); - some_function(); - *x -} -{% endhighlight %} - -These `Retag` instructions are inserted by the compiler pretty much any time -references are copied: At the beginning of every function, all inputs of -reference type get retagged. On every assignment, if the assigned value is of -reference type, it gets retagged. Moreover, we do this even when the reference -value is inside the field of a `struct` or `enum`, to make sure we really cover -all references. (This recursive descent is already implemented, but the -implementation has not landed yet.) However, we do *not* descend recursively -through references: Retagging a `&mut &mut u8` will only retag the *outer* -reference. - -Retagging is the *only* operation that generates fresh tags. Taking a reference -simply forwards the tag of the pointer we are basing this reference on. - -Here is our very first example with explicit retagging: - -{% highlight rust %} -fn demo0() { - let x = &mut 1u8; // nothing interesting happens here - Retag(x); // tag of `x` gets changed to `Uniq(0)` - // stack: [Uniq(0)]; not frozen - - let y = &mut *x; // nothing interesting happens here - Retag(y); // tag of `y` gets changed to `Uniq(1)` - // stack: [Uniq(0), Uniq(1)]; not frozen - - // Check that `Uniq(1)` is on the stack, then pop to bring it to the top. - *y = 5; - // stack: [Uniq(0), Uniq(1)]; not frozen - - // Check that `Uniq(0)` is on the stack, then pop to bring it to the top. - *x = 3; - // stack: [Uniq(0)]; not frozen - - // Check that `Uniq(1)` is on the stack -- it is not, hence UB. - let _val = *y; -} -{% endhighlight %} - -For each reference, `Retag` does the following (we will slightly refine these -instructions later) on all locations covered by the reference (again, according -to `size_of_val`): - -1. Compute a fresh tag, `Uniq(_)` for a mutable reference and `Shr(Some(_))` for - a shared reference. -2. Perform the checks that would also happen when we dereference this reference. -3. Perform the actions that would also happen when an actual access happens - through this reference (for shared references a read access, for mutable - references a write access). -4. If the new tag is `Uniq`, push it onto the stack. (The location cannot be - frozen: `Uniq` tags are only created for mutable references, and we just - performed the actions of a write access to memory, which unfreezes - locations.) -5. If the new tag is `Shr`: - - If the location is already frozen, we do nothing. - - Otherwise: - 1. Push a `Shr` item to the stack. - 2. If the location is outside of `UnsafeCell`, it gets frozen with the - timestamp of the new reference. - -One high-level way to think about retagging is that it computes a fresh tag, and -then performs a reborrow of the old reference with the new tag. - -### 3.2 When Pointers Escape - -Creating a shared reference is not the only way to share a location: We can also -create raw pointers, and if we are careful enough, use them to access a location -from different aliasing pointers. (Of course, "careful enough" is not very -precise, but the precise answer is the very model I am describing here.) - -To account for this, we need one final ingredient in our model: a special -instruction that indicates that a reference was cast to a raw pointer, and may -thus be accessed from these raw pointers in a shared way. Consider the -[following example](https://play.rust-lang.org/?version=stable&mode=debug&edition=2015&gist=253868e96b7eba85ef28e1eabd557f66): - -{% highlight rust %} -fn demo4() { - let x = &mut 1u8; - Retag(x); // tag of `x` gets changed to `Uniq(0)` - // stack: [Uniq(0)]; not frozen - - // Make sure what `x` points to is accessible through raw pointers. - EscapeToRaw(x); - // stack: [Uniq(0), Shr]; not frozen - - let y1 = x as *mut u8; - let y2 = y1; - unsafe { - // All of these first dereference a raw pointer (no checks, tag gets - // ignored) and then perform a read or write access with `Shr(None)` as - // the tag, which is already the top of the stack so nothing changes. - *y1 = 3; - *y2 = 5; - *y2 = *y1; - } - - // Writing to `x` again pops `Shr` off the stack, as per the rules for - // write accesses. - *x = 7; - // stack: [Uniq(0)]; not frozen - - // Any further access through the raw pointers is undefined behavior, even - // reads: The write to `x` re-asserted that `x` is the unique reference for - // this memory. - let _val = unsafe { *y1 }; -} -{% endhighlight %} - -The behavior of `EscapeToRaw` is best described as "reborrowing for a raw -pointer": The steps are the same as for `Retag` above, except that the new -pointer's tag is `Shr(None)` and we do not freeze (i.e., we behave as if the -entire pointee was inside an `UnsafeCell`). - -Knowing about both `Retag` and `EscapeToRaw`, you can now go back to `demo2` and -should be able to fully explain why the stack changes the way it does in that -example. - -### 3.3 The Case of the Aliasing References - -Everything I described so far was pretty much in working condition as of about a -week ago. However, there was one thorny problem that I only discovered fairly -late, and as usual it is best demonstrated by an example -- entirely in safe -code: - -{% highlight rust %} -fn demo_refcell() { - let rc = &mut RefCell::new(23u8); - Retag(rc); // tag gets changed to `Uniq(0)` - // We will consider the stack of the location where `23` is stored; the - // `RefCell` bookkeeping counters are not of interest. - // stack: [Uniq(0)] - - // Taking a shared reference shares the location but does not freeze, due - // to the `UnsafeCell`. - let rc_shr = &*rc; - Retag(rc_shr); // tag gets changed to `Shr(Some(1))` - // stack: [Uniq(0), Shr]; not frozen - - // Lots of stuff happens here but it does not matter for this example. - let mut bmut = rc_shr.borrow_mut(); - - // Obtain a mutable reference into the `RefCell`. - let mut_ref = &mut *bmut; - Retag(mut_ref); // tag gets changed to `Uniq(2)` - // stack: [Uniq(0), Shr, Uniq(2)]; not frozen - - // And at the same time, a fresh shared reference to its outside! - // This counts as a read access through `rc`, so we have to pop until - // at least a `Shr` is at the top of the stack. - let shr_ref = &*rc; // tag gets changed to `Shr(Some(3))` - Retag(shr_ref); - // stack: [Uniq(0), Shr]; not frozen - - // Now using `mut_ref` is UB because its tag is no longer on the stack. But - // that is bad, because it is usable in safe code. - *mut_ref += 19; -} -{% endhighlight %} - -Notice how `mut_ref` and `shr_ref` alias! And yet, creating a shared reference -to the memory already covered by our unique `mut_ref` must not invalidate -`mut_ref`. If we follow the instructions above, when we retag `shr_ref` after -it got created, we have no choice but pop the item matching `mut_ref` off the -stack. Ouch. - -This made me realize that creating a shared reference has to be very weak inside -`UnsafeCell`. In fact, it is entirely equivalent to `EscapeToRaw`: We just have -to make sure some kind of shared access is possible, but we have to accept that -there might be active mutable references assuming exclusive access to the same -locations. That on its own is not enough, though. - -I also added a new check to the retagging procedure: Before taking any action -(i.e., before step 3, which could pop items off the stack), we check if the -reborrow is redundant: If the new reference we want to create is already -dereferencable (because its item is already on the stack and, if applicable, the -stack is already frozen), *and* if the item that justifies this is moreover -"derived from" the item that corresponds to the old reference, then we just do -nothing. Here, "derived from" means "further up the stack". Basically, the -reborrow has already happened and the new reference is ready for use; *and* -because of that "derived from" check, we know that using the new reference will -*not* pop the item corresponding to the old reference off the stack. In that -case, we avoid popping anything, to keep other references valid. - -It may seem like this rule can never apply, because how can our fresh tag match -something that's already on the stack? This is indeed impossible for `Uniq` -tags, but for `Shr` tags, matching is more liberal. For example, this rule -applies in our example above when we create `shr_ref` from `mut_ref`. We do not -require freezing (because there is an `UnsafeCell`), there is already a `Shr` on -the stack (so the new reference is dereferencable) and the item matching the old -reference (`Uniq(0)`) is below that `Shr` (so after using the new reference, the -old one remains dereferencable). Hence we do nothing, keeping the `Uniq(2)` on -the stack, such that the access through `mut_ref` at the end remains valid. - -This may sound like a weird rule, and it is. I would surely not have thought of -this if `RefCell` would not force our hands here. However, as we shall see in -[section 5], it also does not to break any of the important properties of the -model (mutable references being unique and shared references being immutable -except for `UnsafeCell`). Moreover, when pushing an item to the stack (at the -end of the retag action), we can now be sure that the stack is not yet frozen: -if it were frozen, the reborrow would be redundant. - -With this extension, the instructions for retagging and `EscapeToRaw` now look -as follows (again executed on all locations covered by the reference, according -to `size_of_val`): - -1. Compute a fresh tag: `Uniq(_)` for a mutable reference, `Shr(Some(_))` for a - shared reference, `Shr(None)` if this is `EscapeToRaw`. -2. Perform the checks that would also happen when we dereference this reference. - Remember the position of the item matching the tag in the stack. -3. Redundancy check: If the new tag passes the checks performed on a - dereference, and if the item that makes this check succeed is *above* the one - we remembered in step 2 (where the "frozen" state is considered above every - item in the stack), then we stop. We are done for this location. -4. Perform the actions that would also happen when an actual access happens - through this reference (for shared references a read access, for mutable - references a write access).
- Now the location cannot be frozen any more: If the fresh tag is `Uniq`, we - just unfroze; if the fresh tag is `Shr` and the location was already frozen, - then the redundancy check (step 3) would have kicked in. -5. If the new tag is `Uniq`, push it onto the stack. -6. If the new tag is `Shr`, push a `Shr` item to the stack. Then, if the - location is outside of `UnsafeCell`, it gets frozen with the timestamp of the - new reference. - -The one thing I find slightly unsatisfying about the redundancy check is that it -seems to overlap a bit with the rule that on a *read* access, a `Shr` item -matches a `Uniq` tag. Both of these together enable the read-only use of -mutable references that have already been shared; I would prefer to have a -single condition enabling that instead of two working together. Still, overall -I think this is a pleasingly clean model; certainly much cleaner than what I -proposed last year and at the same time much more compatible with existing code. - -## 4 Differences to the Original Proposal -[section 4]: #4-differences-to-the-original-proposal - -The key differences to the original proposal is that the check performed on a -dereference, and the check performed on an access, are not the same check. This -means there are more "moving parts" in the model, but it also means we do not -need a weird special exception (about reads from frozen locations) for `demo1` -any more like the original proposal did. The main reason for this change, -however, is that on an access, we just do not know if we are inside an -`UnsafeCell` or not, so we cannot do all the checks we would like to do. -Accordingly, I also rearranged terminology a bit. There is no longer one -"reactivation" action, instead there is a "deref" check and an "access" action, -as described above in sections [2.2][section 2.2] and [2.3][section 2.3]. - -Beyond that, I made the behavior of shared references and raw pointers more -uniform. This helped to fix test failures around `iter_mut` on slices, which -first creates a raw reference and then a shared reference: In the original -model, creating the shared reference invalidates previously created raw -pointers. As a result of the more uniform treatment, this no longer happens. -(Coincidentally, I did not make this change with the intention of fixing -`iter_mut`. I did this change because I wanted to reduce the number of case -distinctions in the model. Then I realized the relevant test suddenly passed -even with the full model enabled, investigated what happened, and realized I -accidentally had had a great idea. :D ) - -The tag is now "typed" (`Uniq` vs `Shr`) to be able to support `transmute` -between references and shared pointers. Such `transmute` were an open question -in the original model and some people raised concerns about it in the ensuing -discussion. I invite all of you to come up with strange things you think you -should be able to `transmute` and throw them at miri so that we can see if your -use-cases are covered. :) - -Creating a shared reference now always pushes a `Shr` item onto the stack, even -when there is no `UnsafeCell`. This means that starting with a mutable reference -`x`, `&*x as *const _ as *mut _` is pretty much equivalent to `x as *mut _`; the -fact that we have an intermediate shared reference does not matter (not for the -aliasing model, anyway). During the implementation, I realized that in `x as -*const _` on a mutable reference, `x` actually first gets coerced to shared -reference, which then gets cast to a raw pointer. This happens in -`NonNull::from`, so if you later write to that `NonNull`, you end up writing to -a raw pointer that was created from a shared reference. Originally I intended -this to be strictly illegal. This is writing to a shared reference after all, -how dare you! However, it turns out it's actually no big deal *if the shared -reference does not get used again later*. This is an access-based model after -all, if a reference never gets used again we do not care much about enforcing -any guarantees for it. (This is another example of a coincidental fix, where I -had a surprisingly passing test case and then investigated what happened.) - -The redundancy check during retagging can be seen as refining a similar check -that the original model did whenever a new reference was created (where we -wouldn't change the state if the new borrow is already active). - -Finally, the notion of "function barriers" from the original Stacked Borrows has -not been implemented yet. This is the next item on my todo list. - -## 5 Key Properties -[section 5]: #5-key-properties - -Let us look at the two key properties that I set out as design goals, and see -how the model guarantees that they hold true in all valid (UB-free) executions. - -### 5.1 Mutable References are Unique - -The property I would like to establish here is that: After creating (retagging, -really) a `&mut`, if we then run some unknown code *that does not get passed the -reference*, and then we use the reference again (reading or writing), we can be -sure that this unknown code did not access the memory behind our mutable -reference at all (or we have UB). For example: - -{% highlight rust %} -fn demo_mut_unique(our: &mut i32) -> i32 { - Retag(our); // So we can be sure the tag is unique - - *our = 5; - - unknown_code(); - - // We know this will return 5, and moreover if `unknown_code` does not panic - // we know we could do the write after calling `unknown_code` (because it - // cannot even read from `our`). - *our -} -{% endhighlight %} - -The proof sketch goes as follows: After retagging the reference, we know it is -at the top of the stack and the location is not frozen. (The "redundant -reborrow" rule does not apply because a fresh `Uniq` tag can never be -redundant.) For any access performed by the unknown code, we know that access -cannot use the tag of our reference because the tags are unique and not -forgeable. Hence if the unknown code accesses our locations, that would pop our -tag from the stack. When we use our reference again, we know it is on the -stack, and hence has not been popped off. Thus there cannot have been an access -from the unknown code. - -Actually this theorem applies *any time* we have a reference whose tag we can be -sure has not been leaked to anyone else, and which points to locations which -have this tag at the top of the (unfrozen) stack. This is not just the case -immediately after retagging. We know our reference is at the top of the stack -after writing to it, so in the following example we know that `unknown_code_2` -cannot access `our`: - -{% highlight rust %} -fn demo_mut_advanced_unique(our: &mut u8) -> u8 { - Retag(our); // So we can be sure the tag is unique - - unknown_code_1(&*our); - - // This "re-asserts" uniqueness of the reference: After writing, we know - // our tag is at the top of the stack. - *our = 5; - - unknown_code_2(); - - // We know this will return 5 - *our -} -{% endhighlight %} - -### 5.2 Shared References (without `UnsafeCell)` are Immutable - -The key property of shared references is that: After creating (retagging, -really) a shared reference, if we then run some unknown code (it can even have -our reference if it wants), and then we use the reference again, we know that -the value pointed to by the reference has not been changed. For example: - -{% highlight rust %} -fn demo_shr_frozen(our: &u8) -> u8 { - Retag(our); // So we can be sure the tag actually carries a timestamp - - // See what's in there. - let val = *our; - - unknown_code(our); - - // We know this will return `val` - *our -} -{% endhighlight %} - -The proof sketch goes as follows: After retagging the reference, we know the -location is frozen (this is the case even if the "redundant reborrow" rule -applies). If the unknown code does any write, we know this will unfreeze the -location. The location might get re-frozen, but only at the then-current -timestamp. When we do our read after coming back from the unknown code, this -checks that the location is frozen *at least* since the timestamp given in its -tag, so if the location is unfrozen or got re-frozen by the unknown code, the -check would fail. Thus the unknown code cannot have written to the location. - -One interesting observation here for both of these proofs is that all we rely on -when the unknown code is executed are the actions performed on every memory -access. The additional checks that happen when a pointer is dereferenced only -matter in *our* code, not in the foreign code. Hence we have no problem -reasoning about the case where we call some code via FFI that is written in a -language without a notion of "dereferencing", all we care about is the actual -memory accesses performed by that foreign code. This also indicates that we -could see the checks on pointer dereference as another "shadow state operation" -next to `Retag` and `EscapeToRaw`, and then these three operations plus the -actions on memory accesses are all that there is to Stacked Borrows. This is -difficult to implement in miri because dereferences can happen any time a path -is evaluated, but it is nevertheless interesting and might be useful in a -"lower-level MIR" that does not permit dereferences in paths. - -## 6 Evaluation, and How You Can Help -[section 6]: #6-evaluation-and-how-you-can-help - -I have implemented both the validity invariant and the model as described above -in miri. This [uncovered](https://github.com/rust-lang/rust/issues/54908) two -[issues](https://github.com/rust-lang/rust/issues/54957) in the standard -library, but both were related to validity invariants, not Stacked Borrows. -With these exceptions, the model passes the entire test suite. There were some -more test failures in earlier versions (as mentioned in [section 4]), but the -final model accepts all the code covered by miri's test suite. (If you look -close enough, you can see that three libstd methods are currently whitelisted -and what they do is not checked. However, even before I ran into these cases, -[efforts](https://github.com/rust-lang/rust/pull/54668) were already -[underway](https://github.com/rust-lang/rfcs/pull/2582) that would fix all of -them, so I am not concerned about them.) Moreover I wrote a bunch of -compile-fail tests to make sure the model catches various violations of the key -properties it should ensure. - -I am quite happy with this! I was expecting much more trouble, expecting to run -into cases where libstd does strange things that are common or otherwise hard to -declare illegal and that my model could not reasonably allow. I see the test -suite passing as an indication that this model may be well-suited for Rust. - -However, miri's test suite is tiny, and I have but one brain to come up with -counterexamples! In fact I am quite a bit worried because I literally came up -with `demo_refcell` less than two weeks ago, so what else might I have missed? -This where you come in. Please test this model! Come up with something funny -you think should work (I am thinking about funny `transmute` in particular, -using type punning through unions or raw pointers if you prefer that), or maybe -you have some crate that has some unsafe code and a test suite (you do have a -test suite, right?) that might run under miri. - -The easiest way to try the model is the -[playground](https://play.rust-lang.org/): Type the code, select "Tools - Miri", -and you'll see what it does. - -For things that are too long for the playground, you have to install miri on -your own computer. miri depends on rustc nightly and has to be updated -regularly to keep working, so it is not well-suited for crates.io. Instead, -installation instructions for miri are provided -[in the README](https://github.com/solson/miri/#running-miri). We are still -working on making installing miri easier. Please let me know if you are having -trouble with anything. You can report issues, comment on this post or find me -in chat (as of recently, I am partial to Zulip where we have an -[unsafe code guidelines stream](https://rust-lang.zulipchat.com/#narrow/stream/136281-wg-unsafe-code-guidelines)). - -With miri installed, you can `cargo miri` a project with a binary to run it in -miri. Dependencies should be fully supported, so you can use any crate you -like. It is not unlikely, however, that you will run into issues because miri -does not support some operation. In that case please search the -[issue tracker](https://github.com/solson/miri/issues) and report the issue if -it is new. We cannot support everything, but we might be able to do something -for your case. - -Unfortunately, `cargo miri test` is currently broken; if you want to help with -that [here are some details](https://github.com/solson/miri/issues/479). -Moreover, wouldn't it be nice if we could -[run the entire libcore, liballoc and libstd test suite in miri](https://github.com/rust-lang/rust/issues/54914)? -There are tons of interesting cases of Rust's core data structures being -exercise there, and the comparatively tiny miri test suite has already helped to -find two soundness bugs, so there are probably more. Once `cargo miri test` -works again, it would be great to find a way to run it on the standard library -test suites, and set up something so that this happens automatically on a -regular basis (so that we notice regressions). - -As you can see, there is more than enough work for everyone. Don't be shy! I -have a mere two weeks left on this internship, after which I will have to -significantly reduce my Rust activities in favor of finishing my PhD. I won't -disappear entirely though, don't worry -- I will still be able to mentor you if -you want to help with any of the above tasks. :) - -Thanks to @nikomatsakis for feedback on a draft of this post. -