cargo-careful needs nightly

[web.git] / personal / _posts / 2018-11-16-stacked-borrows-implementation.md

diff --git a/personal/_posts/2018-11-16-stacked-borrows-implementation.md b/personal/_posts/2018-11-16-stacked-borrows-implementation.md
index 16a88dfb57349c3ad3f64404018f774832ebbf5f..dbea705eefbe4d9e9518723e9433e9b58901a63d 100644 (file)
--- a/personal/_posts/2018-11-16-stacked-borrows-implementation.md
+++ b/personal/_posts/2018-11-16-stacked-borrows-implementation.md
@@ -4,16 +4,21 @@ categories: internship rust
 forum: https://internals.rust-lang.org/t/stacked-borrows-implemented/8847
 ---
 
 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!
 
 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
 <!-- MORE -->
 
 What Stacked Borrows does is that it defines a semantics for Rust programs such


@@ -29,9 +34,9 @@ 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
 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
 
 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


@@ -147,8 +152,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
 
 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
 [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 +207,7 @@ fn demo2() {
 {% endhighlight %}
 
 If you
 {% 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:
 
 ```
 you will see it complain:
 
 ```


@@ -266,7 +271,7 @@ stack of that location.
 fn demo1() {
   let x = &mut 1u8; // tag: `Uniq(0)`
   // stack: [Uniq(0)]; not frozen
 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
 
   let y1 = &*x; // tag: `Shr(Some(1))`
   // stack: [Uniq(0), Shr]; frozen since 1
 


@@ -314,7 +319,7 @@ fn demo2() {
 
   // 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.
 
   // 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
+  let z = x as *const u8 as *mut u8; // tag erased: `Shr(None)`

   // stack: [Uniq(0), Shr]; frozen since 1
 
   // A write access through a raw pointer: Unfreeze the location and make sure
   // stack: [Uniq(0), Shr]; frozen since 1
 
   // A write access through a raw pointer: Unfreeze the location and make sure


@@ -337,11 +342,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
 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
 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
 
 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


@@ -352,8 +357,7 @@ 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):
 
 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.
+1. If this is a raw pointer, do nothing.  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.
 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.


@@ -370,15 +374,15 @@ covers):
 [section 2.3]: #23-accessing-memory
 
 On an actual memory access, we know the tag of the pointer that was used to
 [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:
+access (we always use the actual tag and disregard the type of the pointer), 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`).
 
 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. 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).


@@ -450,9 +454,10 @@ 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
 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.
+implementation has not landed yet.)  Finally, `Box` is treated like a mutable
+reference, to encode that it asserts unique access.  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.
 
 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.


@@ -482,26 +487,21 @@ fn demo0() {
 }
 {% endhighlight %}
 
 }
 {% 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`):
+For each reference and `Box`, `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.
+1. Compute a fresh tag: `Uniq(_)` for mutable references and `Box`, and
+   `Shr(Some(_))` for shared references.

 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).
 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.
+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.
 
 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 +513,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.)
 
 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 %}
 [following example](https://play.rust-lang.org/?version=stable&mode=debug&edition=2015&gist=253868e96b7eba85ef28e1eabd557f66):
 
 {% highlight rust %}


@@ -524,11 +527,11 @@ fn demo4() {
   Retag(x); // tag of `x` gets changed to `Uniq(0)`
   // stack: [Uniq(0)]; not frozen
 
   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.
   // 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
   // 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
   let y2 = y1;
   unsafe {
     // All of these first dereference a raw pointer (no checks, tag gets


@@ -551,14 +554,19 @@ fn demo4() {
 }
 {% endhighlight %}
 
 }
 {% 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.

 
 

-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.
+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 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
 
 
 ### 3.3 The Case of the Aliasing References
 


@@ -569,7 +577,7 @@ code:
 
 {% highlight rust %}
 fn demo_refcell() {
 
 {% highlight rust %}
 fn demo_refcell() {

-  let rc = &mut RefCell::new(23u8);
+  let rc: &mut RefCell<u8> = &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.
   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.


@@ -577,22 +585,22 @@ fn demo_refcell() {
 
   // Taking a shared reference shares the location but does not freeze, due
   // to the `UnsafeCell`.
 
   // Taking a shared reference shares the location but does not freeze, due
   // to the `UnsafeCell`.

-  let rc_shr = &*rc;
+  let rc_shr: &RefCell<u8> = &*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.
   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();
+  let mut bmut: RefMut<u8> = rc_shr.borrow_mut();

   
   // Obtain a mutable reference into the `RefCell`.
   
   // Obtain a mutable reference into the `RefCell`.

-  let mut_ref = &mut *bmut;
+  let mut_ref: &mut u8 = &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.
   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))`
+  let shr_ref: &RefCell<u8> = &*rc; // tag gets changed to `Shr(Some(3))`

   Retag(shr_ref);
   // stack: [Uniq(0), Shr]; not frozen
 
   Retag(shr_ref);
   // stack: [Uniq(0), Shr]; not frozen
 


@@ -609,10 +617,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
 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
 
 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


@@ -644,28 +652,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.
 
 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 a mutable reference, `Shr(Some(_))` for a
-   shared reference, `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
 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.
 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
 
 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


@@ -704,25 +712,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
 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. :)
 
 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).
 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).


@@ -831,22 +823,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"
 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
 
 ## 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
 [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
 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


@@ -855,37 +847,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.
 
 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.
 
 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
 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.
 
 
 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,
 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
 [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)).
 
 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
 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


@@ -896,11 +897,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
 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).
 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
 
 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


@@ -908,7 +910,21 @@ 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. :)
 
 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
+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
+PRs at unparalleled speed. <3
+
+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](https://internals.rust-lang.org/t/stacked-borrows-implemented/8847).
 help or report results of your experiments, if you have any questions or
 comments, please join the
 [discussion in the forums](https://internals.rust-lang.org/t/stacked-borrows-implemented/8847).

+
+## Changelog
+
+**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.