From 187a862323d9120c30bd4824ad6f8760e84c91a4 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Sat, 22 Dec 2018 13:44:51 +0100 Subject: [PATCH] update Stacked Borrows post to (almost) current model --- ...18-11-16-stacked-borrows-implementation.md | 162 +++++++++--------- 1 file changed, 79 insertions(+), 83 deletions(-) diff --git a/personal/_posts/2018-11-16-stacked-borrows-implementation.md b/personal/_posts/2018-11-16-stacked-borrows-implementation.md index df60719..35bf735 100644 --- a/personal/_posts/2018-11-16-stacked-borrows-implementation.md +++ b/personal/_posts/2018-11-16-stacked-borrows-implementation.md @@ -147,8 +147,8 @@ fn demo0() { 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 +[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 @@ -202,7 +202,7 @@ fn demo2() { {% endhighlight %} If you -[try this in miri](https://play.rust-lang.org/?version=stable&mode=debug&edition=2015&gist=1bc8c2f432941d02246fea0808e2e4f4), +[try this in Miri](https://play.rust-lang.org/?version=stable&mode=debug&edition=2015&gist=1bc8c2f432941d02246fea0808e2e4f4), you will see it complain: ``` @@ -266,7 +266,7 @@ stack of that location. 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 @@ -337,11 +337,11 @@ 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: +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. +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 @@ -492,16 +492,11 @@ refine these instructions later) on all locations covered by the 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. +4. Check if the new tag is `Shr(Some(t))` and the location is inside an `UnsafeCell`. + - If both conditions apply, freeze the location with timestamp `t`. If it + is already frozen, do nothing. + - Otherwise, push a new item onto the stack: `Shr` if the tag is a `Shr(_)`, + `Uniq(id)` if the tag is `Uniq(id)`. 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. @@ -513,9 +508,12 @@ 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 +To account for this, we consider the act of casting to a raw pointer as a +special way of creating a reference +(["creating a raw reference"](https://github.com/rust-lang/rfcs/pull/2582), so +to speak). As usual for creating a new reference, that operation is followed by +retagging. This retagging is special though because unlike normal retagging it +acts on raw pointers. Consider the [following example](https://play.rust-lang.org/?version=stable&mode=debug&edition=2015&gist=253868e96b7eba85ef28e1eabd557f66): {% highlight rust %} @@ -524,11 +522,11 @@ fn demo4() { Retag(x); // tag of `x` gets changed to `Uniq(0)` // stack: [Uniq(0)]; not frozen + let y1 = x as *mut u8; // Make sure what `x` points to is accessible through raw pointers. - EscapeToRaw(x); + Retag([raw] y1) // tag of `y` gets erased to `Shr(None)` // stack: [Uniq(0), Shr]; not frozen - - let y1 = x as *mut u8; // tag erased: `Shr(None)` + let y2 = y1; unsafe { // All of these first dereference a raw pointer (no checks, tag gets @@ -551,19 +549,19 @@ fn demo4() { } {% 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`). +`Retag([raw])` acts almost like a normal retag, except that it does not ignore +raw pointers and instead tags them `Shr(None)`, and pushes `Shr` to the stack. -This is needed, because when casting a reference to a raw pointer (and actually, -on any cast involving pointers), the tag gets erased, meaning it gets reset to -`Shr(None)`. Thanks to `EscapeToRaw`, there is a matching `Shr` on the stack, -making sure the raw pointer can actually be used. +This way, even if the program casts the pointer to an integer and back (where we +cannot always keep track of the tag, so it might get reset to `Shr(None)`), +there is a matching `Shr` on the stack, making sure the raw pointer can actually +be used. One way to think about this is to consider the reference to "escape" +when it is cast to a raw pointer, which is reflected by the `Shr` item on the +stack. -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. +Knowing about how `Retag` interacts with raw pointers, 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 @@ -614,10 +612,10 @@ 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. +`UnsafeCell`. In fact, it is entirely equivalent to `Retag([raw])`: 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 @@ -649,28 +647,28 @@ 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`): +With this extension, the instructions for `Retag` 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 mutable references and `Box`, - `Shr(Some(_))` for shared references, `Shr(None)` if this is `EscapeToRaw`. +1. Compute a fresh tag: `Uniq(_)` for mutable references, `Box`, `Shr(Some(_))` + for shared references, and `Shr(None)` for raw pointers. 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. + item in the stack), then 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. +5. Check if the new tag is `Shr(Some(t))` and the location is inside an `UnsafeCell`. + - If both conditions apply, freeze the location with timestamp `t`. If it + is already frozen, do nothing. + - Otherwise, push a new item onto the stack: `Shr` if the tag is a `Shr(_)`, + `Uniq(id)` if the tag is `Uniq(id)`. 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 @@ -709,25 +707,9 @@ 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 +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). @@ -836,22 +818,22 @@ 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. +next to `Retag`, and then these two 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 +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 +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 @@ -860,37 +842,46 @@ 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 +The most interesting change I had to make to libstd is +[in `NonNull::from`](https://github.com/rust-lang/rust/pull/56161). That +function turned a `&mut T` into a `*const T` going through a `&T`. This means +that the final raw pointer was created from a shared reference, and hence must +not be used for mutation. An earlier version of this post described a model +that would permit such behavior, but I think we should actually at least +experiment with ruling it out: "no mutation through (pointers derived from) +shared references" is an old rule in Rust, after all. + +Overall, 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 +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. +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 +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 +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 +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 +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 @@ -901,11 +892,12 @@ 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 +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). +**Update:** `cargo miri test` has been fixed in the mean time, so you can use it on your libraries now! **/Update** 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 @@ -914,7 +906,7 @@ 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, to @shepmaster for -making miri available on the playground, and to @oli-obk for reviewing all my +making Miri available on the playground, and to @oli-obk for reviewing all my PRs at unparalleled speed. <3 If you want to @@ -927,3 +919,7 @@ comments, please join the **2018-11-21:** 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. + +**2018-12-22:** Creating a shared reference does not push a `Shr` item to the +stack (unless there is an `UnsafeCell`). Moreover, creating a raw pointer is a +special kind of retagging. -- 2.30.2