From fa5fd668ce14aa7d5c5a6fa377fa3dddc7570af1 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Fri, 16 Nov 2018 17:52:59 +0100 Subject: [PATCH] finalize and publish post --- ...8-11-16-stacked-borrows-implementation.md} | 210 ++++++++++-------- 1 file changed, 115 insertions(+), 95 deletions(-) rename personal/{_drafts/stacked-borrows-implementation.md => _posts/2018-11-16-stacked-borrows-implementation.md} (82%) diff --git a/personal/_drafts/stacked-borrows-implementation.md b/personal/_posts/2018-11-16-stacked-borrows-implementation.md similarity index 82% rename from personal/_drafts/stacked-borrows-implementation.md rename to personal/_posts/2018-11-16-stacked-borrows-implementation.md index 1bc1ef1..211d21d 100644 --- a/personal/_drafts/stacked-borrows-implementation.md +++ b/personal/_posts/2018-11-16-stacked-borrows-implementation.md @@ -27,10 +27,10 @@ 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 try to explain at least parts of this model 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. +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 @@ -63,7 +63,10 @@ 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. +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 @@ -81,16 +84,16 @@ 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 tags, indicating +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, and every byte occupied by the -pointer has a stack regulating access to this location. Remember, -[a byte is more than a `u8`]({% post_url 2018-07-24-pointers-and-bytes %}). -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 +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 @@ -104,11 +107,12 @@ 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 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.) +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 +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. @@ -150,10 +154,11 @@ 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; - | ^^ Encountered reference with non-reactivatable tag: Borrow-to-reactivate Uniq(1245) does not exist on the stack + | ^^ Borrow being dereferenced (Uniq(1037)) does not exist on the stack | ``` @@ -290,7 +295,7 @@ fn demo1() { 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 (whether you have a `*`, also implicitly), and actual +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*. @@ -338,8 +343,9 @@ 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 (we might have raw or shared pointers with a unique tag, for example). +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 @@ -368,7 +374,7 @@ access (unless it was a raw pointer, in which case the tag we see is 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 +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. @@ -384,11 +390,10 @@ 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 only thing that is subtle and potentially surprising 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. +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 @@ -413,12 +418,11 @@ 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 (and the -exception for matching `Uniq` tags with `Shr` items on reads does not affect -this property). 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. +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 @@ -456,11 +460,11 @@ Here is our very first example with explicit retagging: {% highlight rust %} fn demo0() { - let x = &mut 1u8; + 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; + 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 @@ -552,7 +556,7 @@ 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 not that +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 @@ -603,11 +607,11 @@ to the memory already covered by our unique `mut_ref` must not invalidate 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 when -on locations 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. +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 @@ -616,10 +620,10 @@ 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. +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` @@ -636,8 +640,8 @@ 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 be sure that the stack is not yet frozen: if it -were frozen, the reborrow would be redundant. +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 @@ -653,9 +657,9 @@ to `size_of_val`): 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). + 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 + 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 @@ -666,7 +670,9 @@ 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. +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 @@ -674,13 +680,13 @@ single condition enabling that instead of two working together. 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 for `demo1` any more like the original proposal -did. The main reason for this, 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]. +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 @@ -702,18 +708,19 @@ 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`. This -came up during the implementation because 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.) +`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 @@ -732,10 +739,9 @@ how the model guarantees that they hold true in all valid (UB-free) executions. 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* nor do we derive another reference from ours, 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: +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 { @@ -819,13 +825,16 @@ 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. This 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. +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 @@ -836,9 +845,19 @@ in miri. This [uncovered](https://github.com/rust-lang/rust/issues/54908) two 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. Moreover I wrote -a bunch of compile-fail tests to make sure the model catches various violations -of the key properties it should ensure. +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 @@ -855,12 +874,12 @@ 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 currently on crates.io. Installation -instructions for miri are provided -[in the README](https://github.com/solson/miri/#running-miri). 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 +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 @@ -873,16 +892,17 @@ 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? 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). +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 three weeks left on this internship, after which I will have to +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. :) -- 2.30.2