forum: https://internals.rust-lang.org/t/stacked-borrows-implemented/8847
---
-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
+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]({%
+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!
+This post is a self-contained introduction to Stacked Borrows. Other than
+historical curiosity and some comparison with my earlier work on
+[Types as Contracts]({% post_url 2017-07-17-types-as-contracts %}) there is no
+reason to read the [original post]({% post_url 2018-08-07-stacked-borrows %}) at
+this point.
+
<!-- MORE -->
What Stacked Borrows does is that it defines a semantics for Rust programs such
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.
+be the same as [last time]({% post_url 2018-08-07-stacked-borrows %}), 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
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
{% 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:
```
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
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
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.
+2. Otherwise, if this is a write access, unfreeze the location (set
+ `frozen_since` to `None`). (If this is a read access and we come here, the
+ location is already unfrozen.)
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).
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.
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 %}
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
}
{% 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
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
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).<br>
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
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).
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
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
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
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
**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.
projects / web.git / blobdiff