(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 read-only (we can rely on no writes happening to the
+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
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](#4-differences-to-the-original-proposal). If you only want to know
-how to help, jump to [section 6](#6-evaluation-and-how-you-can-help).
+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 read-only and focus on
+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:
referring to the borrow checker, because we want to have rules that also work
for unsafe code.
-To be able to do this, we have to pretend our machine has two thing which real
+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
## 2 Enabling Sharing
-If we just had unique pointers, Rust would be a rather dull language. Lucky
-enough, there are also two ways to have shared access to a location: Through
+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 read-only.
+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
{% 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
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).
-The following checks are done on every pointer dereference:
+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 of every location this reference points to (the size is
- determine with `size_of_val`).
+ 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 of every location.
-5. If the tag is `Shr(Some(t))`, then the check depends on whether a location is
- inside an `UnsafeCell` or not, according to the type of the reference.
+ 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:
+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`).
+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, popping the stack, we make it empty, then we have undefined behavior.
+ 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
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 turns, is good because we might use it for optimizations).
+(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
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. However, we do *not* descend recursively through references:
-Retagging a `&mut &mut u8` will only retag the *outer* reference.
+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.
// stack: [Uniq(0)]; not frozen
let y = &mut *x;
- Retag(x); // tag of `y` gets changed to `Uniq(1)`
+ 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.
}
{% endhighlight %}
-For each reference, `Retag` does the following (with one special exception that
-will be explained later):
+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. 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
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
+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):
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 special exception: When "creating a raw reference"
-(`EscapeToRaw`, or `Retag` on a shared reference when we are inside an
-`UnsafeCell`), we still first check that the pointer this reference is created
-one is allowed to be dereferenced -- and we remember the position of the item on
-the stack that justifies this, let's call this `ptr_idx`. Remember, that does
-not change the stack, so it has no adverse effect in `demo_refcell`. Next, we do
-a very peculiar check:
-
-1. Determine if the new reference we are creating (it will have a `Shr` tag) is
- *already dereferencable*. This is possible, for example, if the location
- already got shared previously. This is also the case in `demo_refcell`:
- Creating `rc_shr` pushed a `Shr` onto the stack. We again remember the
- position of the item that justifies this, let's call it `new_idx`.
-
- - If this is the case, we moreover *compare* the `new_idx` and `ptr_idx`.
- If `new_idx` is *above* `ptr_idx` on the stack, that means that not only
- is the location already being shared (so we can dereference with our new
- `Shr` tag), moreover *the pointer we create this reference from has
- already been shared*. The new pointer is already "derived from" the one
- this reference is based on. Basically, everything that we wanted to do
- while creating this reference has already happened. In this case, we just
- do nothing else: We leave the stacks unchanged.
-
- - Otherwise, we continue as usual.
-
-This rule has the effect that in our example above, when we create `shr_ref`, we
-do not pop `Uniq(2)` off the stack, and hence the access through `mut_ref` at
-the end remains valid.
-
-This may sound like a weird special case, and it is. I would surely not have
-thought of this if `RefCell` would not force our hands here. However, it also
-does not seem to break any of the important properties of the model (mutable
-references being unique and shared references being read-only except for
-`UnsafeCell`).
+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 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.
## 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
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.
+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 part of unifying the two, this happens no longer.
+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
guarantees for it. (This is another example of a coincidental fix, where I had
a surprisingly passing test case and then investigated what happened.)
-And finally, there is this special exception about creating raw references, to
-fix `demo_refcell`.
+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.
{% 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. 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.
+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
}
{% endhighlight %}
-### 5.2 Shared References (without `UnsafeCell)` are Read-only
+### 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
{% endhighlight %}
The proof sketch goes as follows: After retagging the reference, we know the
-location is frozen. 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.
+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
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
+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.
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.
+<!-- If you want to help or report results of your experiments, if you have any questions or comments, please join the [discussion in the forums](). -->
projects / web.git / blobdiff