From: Ralf Jung <post@ralfj.de>
Date: Mon, 12 Nov 2018 19:38:41 +0000 (+0100)
Subject: First draft of stacked borows impl post
X-Git-Url: https://git.ralfj.de/web.git/commitdiff_plain/8bc0d478090b594c80adebad51cc1ef02b8814db?ds=sidebyside;hp=be7181b97194b50d240282729129bd0775cfc0c3

First draft of stacked borows impl post
---

diff --git a/personal/_drafts/stacked-borrows-implementation.md b/personal/_drafts/stacked-borrows-implementation.md
new file mode 100644
index 0000000..029b0be
--- /dev/null
+++ b/personal/_drafts/stacked-borrows-implementation.md
@@ -0,0 +1,815 @@
+---
+title: "Stacked Borrows Implemented"
+categories: internship rust
+---
+
+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
+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!
+
+<!-- MORE -->
+
+What Stacked Borrows does is that it defines a semantics for Rust programs such
+that some things about references always hold true for every valid execution
+(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
+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
+help us.  We have to define a set of rules that makes sense even for unsafe
+code.
+
+I will try to explain at least parts of this model again in this post.  The
+explanation is not going to be the same as last time, not only because it
+changed a bit, but also because I think I understand the model better myself
+now.
+
+Ready?  Let's get started.  I hope you brought some time, because this is a
+rather lengthy post.  If you are not interested in the details, you can skip
+right to section 4.  If you only want to know how to help, go to section 6.
+
+## 1 Enforcing Uniqueness
+
+Let us first ignore the part about `&` references being read-only 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:
+
+{% highlight rust %}
+fn demo0() {
+  let x = &mut 1u8;
+  let y = &mut *x;
+  *y = 5;
+  // Write through a pointer aliasing `y`
+  *x = 3;
+  // Use `y` again, asserting it is still exclusive
+  let _val = *y;
+}
+{% endhighlight %}
+
+We want this function to be disallowed because between two uses of `y`, there is
+a use of another pointer for the same location, violating the fact that `y`
+should be unique.
+
+Notice that this function does not compile, the borrow checker won't allow it.
+That's great!  It is undefined behavior, after all.  But the entire point of
+this exercise is to explain *why* we have undefined behavior here *without*
+referring to the borrow checker, because we want to have rules that also work
+for unsafe code.
+
+To be able to do this, we have to pretend our machine has two thing 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
+source languages make distinctions that do not appear in the actual hardware.  A
+related example is
+[valgrind's memcheck](http://valgrind.org/docs/manual/mc-manual.html) which
+keeps track of which memory is initialized to be able to detect memory errors:
+During a normal execution, uninitialized memory looks just like all other
+memory, but to figure out whether the program is violating C's memory rules, we
+have to keep track of some extra state.
+
+For stacked borrows, the extra state looks as follows:
+
+1. For every pointer, we keep track of an extra "tag" that records when and how
+   this pointer was created.
+2. For every location in memory, we keep track of a stack of tags, indicating
+   which tag a pointer must have to be allowed to access this location.
+
+These exist separately, i.e., when a pointer is stored in memory, then we both
+have a tag stored as part of this pointer value, and every byte occupied by the
+pointer has a stack regulating access to this location.  Remember,
+[a byte is more than a `u8`]({% post_url 2018-07-24-pointers-and-bytes %}).
+Also these two do not interact, i.e., when loading a pointer from memory, we
+just load the tag that was stored as part of this pointer.  The stack of a
+location, and the tag of a pointer stored at some location, do not have any
+effect on each other.
+
+In our example, there are two pointers (`x` and `y`) and one location of
+interest (the one both of these pointers point to, initialized with `1u8`).
+When we initially create `x`, it gets tagged `Uniq(0)` to indicate that it is a
+unique reference, and the location's stack has `Uniq(0)` at its top to indicate
+that this is the latest reference allowed to access said location.  When we
+create `y`, it gets a new tag, `Uniq(1)`, so that we can distinguish it from
+`x`.  We also push `Uniq(1)` onto the stack, indicating not only that `Uniq(1)`
+is the latest reference allow to access, but also that it is "derived from"
+`Uniq(0)`: The tags higher up in the stack are descendants of the ones further
+down.
+
+So we have: `x` tagged `Uniq(0)`, `y` tagged `Uniq(1)`, and the stack contains
+`[Uniq(0), Uniq(1)]`. (Top of the stack is on the right.)
+
+When we use `y` to access the location, we make sure its tag is at the top of
+the stack: Check, no problem here.  When we use `x`, we do the same thing: Since
+it is not at the top yet, we pop the stack until it is, which is easy.  Now the
+stack is just `[Uniq(0)]`.  Now we use `y` again and... blast!  Its tag is not
+on the stack.  We have undefined behavior.
+
+Well, actually that 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
+[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
+have to improve that one):
+
+```
+ --> src/main.rs:6:14
+  |
+6 |   let _val = *y;
+  |              ^^ Encountered reference with non-reactivatable tag: Borrow-to-reactivate Uniq(1245) does not exist on the stack
+  |
+```
+
+## 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
+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.
+
+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
+this is not undefined behavior:
+
+{% highlight rust %}
+fn demo1() {
+  let x = &mut 1u8;
+  // Create several shared references, and we can also still read from `x`
+  let y1 = &*x;
+  let _val = *x;
+  let y2 = &*x;
+  let _val = *y1;
+  let _val = *y2;
+}
+{% endhighlight %}
+
+However, the following code is *not* okay:
+
+{% highlight rust %}
+fn demo2() {
+  let x = &mut 1u8;
+  let y = &*x;
+  // Create raw reference aliasing `y` and write through it
+  let z = x as *const u8 as *mut u8;
+  unsafe { *z = 3; }
+  // Use `y` again, asserting it still points to the same value
+  let _val = *y;
+}
+{% endhighlight %}
+
+If you
+[try this in miri](https://play.rust-lang.org/?version=stable&mode=debug&edition=2015&gist=1bc8c2f432941d02246fea0808e2e4f4),
+you will see it complain:
+
+```
+ --> src/main.rs:6:14
+  |
+6 |   let _val = *y;
+  |              ^^ Location is not frozen long enough
+  |
+```
+
+How is it doing that, and what is a "frozen" location?
+
+To explain this, we have to extend the "shadow state" of our "virtual machine" a
+bit.  First of all, we introduce a new kind of tag that a pointer can carry: A
+*shared* tag.  The following Rust type describes the possible tags of a pointer:
+
+{% highlight rust %}
+pub type Timestamp = u64;
+pub enum Borrow {
+    Uniq(Timestamp),
+    Shr(Option<Timestamp>),
+}
+{% endhighlight %}
+
+You can think of the timestamp as a unique ID, but as we will see, for shared
+references, it is also important to be able to determine which of these IDs was
+created first.  The timestamp is optional in the shared tag because that tag is
+also used by raw pointers, and for raw pointers, we are often not able to track
+when and how they are created (for example, when raw pointers are converted to
+integers and back).
+
+We use a separate type for the items on our stack, because there we do not need
+a timestamp for shared pointers:
+
+{% highlight rust %}
+pub enum BorStackItem {
+    Uniq(Timestamp),
+    Shr,
+}
+{% endhighlight %}
+
+And finally, a "borrow stack" consists of a stack of `BorStackItem`, together
+with an indication of whether the stack (and the location it governs) is
+currently *frozen*, meaning it may only be read, not written:
+
+{% highlight rust %}
+pub struct Stack {
+    borrows: Vec<BorStackItem>, // used as a stack; never empty
+    frozen_since: Option<Timestamp>, // virtual frozen "item" on top of the stack
+}
+{% endhighlight %}
+
+### 2.1 Executing the Examples
+
+Let us now look at what happens when we execute our two example programs.  To
+this end, I will embed comments in the source code.  There is only one location
+of interest here, so whenever I talk about a "stack", it's the stack of that
+location.
+
+{% highlight rust %}
+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
+
+  // Access through `x`.  We first check whether its tag `Uniq(0)` is in the
+  // stack (it is).  Next, we make sure that either our item *or* `Shr` is on
+  // top *or* the location is frozen.  The latter is the case, so we go on.
+  let _val = *x;
+  // stack: [Uniq(0), Shr]; frozen since 1
+
+  // This is not an access, but we still dereference `x`, so we do the same
+  // actions as on a read.  Just like in the previous line, nothing happens.
+  let y2 = &*x; // tag: `Shr(Some(2))`
+  // stack: [Uniq(0), Shr]; frozen since 1
+
+  // Access through `y1`.  Since the shared tag has a timestamp (1) and the type
+  // (`u8`) does not allow interior mutability (no `UnsafeCell`), we check that
+  // the location is frozen since (at least) that timestamp.  It is.
+  let _val = *y1;
+  // stack: [Uniq(0), Shr]; frozen since 1
+
+  // Same as with `y2`: The location is frozen at least since 2 (actually, it
+  // is frozen since 1), so we are good.
+  let _val = *y2;
+  // stack: [Uniq(0), Shr]; frozen since 1
+}
+{% endhighlight %}
+
+This example demonstrates a few new aspects.  First of all, there are actually
+two operations that perform tag-related checks in this model (so far):
+Dereferencing a pointer (whether you have a `*`, also implicitly), and actual
+memory accesses.  Operations like `&*x` are an example of operations that
+dereference a pointer without accessing memory.  Secondly, *reading* through a
+mutable reference is actually okay *even when that reference is not exclusive*.
+It is only *writing* through a mutable reference that "re-asserts" its
+exclusivity.  I will come back to these points later, but let us first go
+through another example.
+
+{% highlight rust %}
+fn demo2() {
+  let x = &mut 1u8; // tag: `Uniq(0)`
+  // stack: [Uniq(0)]; not frozen
+  
+  let y = &*x; // tag: `Shr(Some(1))`
+  // stack: [Uniq(0), Shr]; frozen since 1
+
+  // 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
+  // stack: [Uniq(0), Shr]; frozen since 1
+
+  // A write access through a raw pointer: Unfreeze the location and make sure
+  // that `Shr` is at the top of the stack.
+  unsafe { *z = 3; }
+  // stack: [Uniq(0), Shr]; not frozen
+
+  // Access through `y`.  There is a timestamp in the `Shr` tag, and the type
+  // `u8` does not allow interior mutability, but the location is not frozen.
+  // This is undefined behavior.
+  let _val = *y;
+}
+{% endhighlight %}
+
+### 2.2 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
+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:
+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.
+
+Notice that on a dereference, we have *both* a tag at the pointer *and* the type
+of a pointer, and the two might not agree which we do not always want to rule
+out (we might have raw or shared pointers with a unique tag, for example).
+
+The following checks are done on every pointer dereference:
+
+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`).
+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.
+    - 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
+
+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:
+
+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`).
+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.
+
+To understand these rules better, try going back through the three examples we
+have seen so far and applying these rules for dereferencing pointers and
+accessing memory to understand how they interact.
+
+The only thing that is subtle and potentially surprising here is that we make a
+`Uniq` tag match a `Shr` item and also accept `Uniq` reads on frozen locations.
+This is required to make `demo1` work: Rust permits read accesses through
+mutable references even when they are not currently actually unique.  Our model
+hence has to do the same.
+
+## 3 Retagging and Creating Raw Pointers
+
+We have talked quite a bit about what happens when we *use* a pointer.  It is
+time we take a close look at *how pointers are created*.  However, before we go
+there, I would like us to consider one more example:
+
+{% highlight rust %}
+fn demo3(x: &mut u8) -> u8 {
+    some_function();
+    *x
+}
+{% endhighlight %}
+
+The question is: Can we move the load of `x` to before the function call?
+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).
+Unfortunately, things are not so easy.
+
+The uniqueness of mutable references entirely rests on the fact that the pointer
+has a unique tag: If our tag is at the top of the stack (and the location is not
+frozen), then any access with another tag will pop our item from the stack (or
+cause undefined behavior).  This is ensured by the memory access checks (and the
+exception for matching `Uniq` tags with `Shr` items on reads does not affect
+this property).  Hence, if our tag is *still* on the stack after some other
+accesses happened (and we know it is still on the stack every time we
+dereference the pointer, as per the dereference checks described above), we know
+that no access through a pointer with a different tag can have happened.
+
+### 3.1 Guaranteed Freshness
+
+However, what if `some_function` has an exact copy of `x`?  We got `x` from our
+caller (whom we do not trust), maybe they used that same tag for another
+reference (copied it with `transmute_copy` or so) and gave that to
+`some_function`?  There is a simple way we can circumvent this concern: Generate
+a new tag for `x`.  If *we* generate the tag (and we know generation never emits
+the same tag twice, which is easy), we can be sure this tag is not used for any
+other reference.  So let us make this explicit by putting a `Retag` instruction
+into the code where we generate new tags:
+
+{% highlight rust %}
+fn demo3(x: &mut u8) -> u8 {
+    Retag(x);
+    some_function();
+    *x
+}
+{% endhighlight %}
+
+These `Retag` instructions are inserted by the compiler pretty much any time
+references are copied: At the beginning of every function, all inputs of
+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.
+
+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.
+
+Here is our very first example with explicit retagging:
+
+{% highlight rust %}
+fn demo0() {
+  let x = &mut 1u8;
+  Retag(x); // tag of `x` gets changed to `Uniq(0)`
+  // stack: [Uniq(0)]; not frozen
+  
+  let y = &mut *x;
+  Retag(x); // 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.
+  *y = 5;
+  // stack: [Uniq(0), Uniq(1)]; not frozen
+
+  // Check that `Uniq(0)` is on the stack, then pop to bring it to the top.
+  *x = 3;
+  // stack: [Uniq(0)]; not frozen
+
+  // Check that `Uniq(1)` is on the stack -- it is not, hence UB.
+  let _val = *y;
+}
+{% endhighlight %}
+
+For each reference, `Retag` does the following (with one special exception that
+will be explained later):
+
+1. Compute a fresh tag, `Uniq(_)` for a mutable reference and `Shr(Some(_))` for
+   a shared reference.
+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.
+
+### 3.2 When Pointers Escape
+
+Creating a shared reference is not the only way to share a location: We can also
+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
+[following example](https://play.rust-lang.org/?version=stable&mode=debug&edition=2015&gist=253868e96b7eba85ef28e1eabd557f66):
+
+{% highlight rust %}
+fn demo4() {
+  let x = &mut 1u8;
+  Retag(x); // tag of `x` gets changed to `Uniq(0)`
+  // stack: [Uniq(0)]; not frozen
+
+  // Make sure what `x` points to is accessible through raw pointers.
+  EscapeToRaw(x);
+  // 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
+    // ignored) and then perform a read or write access with `Shr(None)` as
+    // the tag, which is already the top of the stack so nothing changes.
+    *y1 = 3;
+    *y2 = 5;
+    *y2 = *y1;
+  }
+
+  // Writing to `x` again pops `Shr` off the stack, as per the rules for
+  // write accesses.
+  *x = 7;
+  // stack: [Uniq(0)]; not frozen
+
+  // Any further access through the raw pointers is undefined behavior, even
+  // reads: The write to `x` re-asserted that `x` is the unique reference for
+  // this memory.
+  let _val = unsafe { *y1 };
+}
+{% 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`).
+
+Knowing about both `Retag` and `EscapeToRaw`, you can now go back to `demo2` and
+should be able to fully explain why the stack changes the way it does not that
+example.
+
+### 3.3 The Case of the Aliasing References
+
+Everything I described so far was pretty much in working condition as of about a
+week ago.  However, there was one thorny problem that I only discovered fairly
+late, and as usual it is best demonstrated by an example -- entirely in safe
+code:
+
+{% highlight rust %}
+fn demo_refcell() {
+  let rc = &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.
+  // stack: [Uniq(0)]
+
+  // Taking a shared reference shares the location but does not freeze, due
+  // to the `UnsafeCell`.
+  let rc_shr = &*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.
+  let mut bmut = rc_shr.borrow_mut();
+  
+  // Obtain a mutable reference into the `RefCell`.
+  let mut_ref = &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.
+  let shr_ref = &*rc; // tag gets changed to `Shr(Some(3))`
+  Retag(shr_ref);
+  // stack: [Uniq(0), Shr]; not frozen
+
+  // Now using `mut_ref` is UB because its tag is no longer on the stack.  But
+  // that is bad, because it is usable in safe code.
+  *mut_ref += 19;
+}
+{% endhighlight %}
+
+Notice how `mut_ref` and `shr_ref` alias!  And yet, creating a shared reference
+to the memory already covered by our unique `mut_ref` must not invalidate
+`mut_ref`.  If we follow the instructions above, when we retag `shr_ref` after
+it got created, we have no choice but pop the item matching `mut_ref` off the
+stack.  Ouch.
+
+This made me realize that creating a shared reference has to be very weak when
+on locations inside `UnsafeCell`.  In fact, it is entirely equivalent to
+`EscapeToRaw`: We just have to make sure some kind of shared access is possible,
+but we have to accept that there might be active mutable references assuming
+exclusive access to the same locations.  That on its own is not enough, though.
+
+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`).
+
+## 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
+means there are more "moving parts" in the model, but it also means we do not
+need a weird special exception for `demo1` any more like the original proposal
+did.  The main reason for this, however, is that on an access, we just do not
+know if we are inside an `UnsafeCell` or not, so we cannot do all the checks we
+would like to do.
+
+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.
+(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
+even with the full model enabled, investigated what happened, and realized I
+accidentally had had a great idea. :D )
+
+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
+use-cases are covered. :)
+
+Creating a shared reference now always pushes a `Shr` item onto the stack, even
+when there is no `UnsafeCell`. This means that starting with a mutable reference
+`x`, `&*x as *const _ as *mut _` is pretty much equivalent to `x as *mut`.  This
+came up during the implementation because I realized that in `x as *const _` on
+a mutable reference, `x` actually first gets coerced to shared reference, which
+then gets cast to a raw pointer.  This happens in `NonNull::from`, so if you
+later write to that `NonNull`, you end up writing to a raw pointer that was
+created from a shared reference.  Originally I intended this to be strictly
+illegal.  This is writing to a shared reference after all, how dare you!
+However, it turns out it's actually no big deal *if the shared reference does
+not get used again later*.  This is an access-based model after all, if a
+reference never gets used again we do not care much about enforcing any
+guarantees for it.  (This is another example of a coincidental fix, where I had
+a surprisingly passing test case and then investigated what happened.)
+
+And finally, there is this special exception about creating raw references, to
+fix `demo_refcell`.
+
+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
+
+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.
+
+### 5.1 Mutable References are Unique
+
+The property I would like to establish here is that: After creating (retagging,
+really) a `&mut`, if we then run some unknown code *that does not get passed the
+reference* nor do we derive another reference from ours, and then we use the
+reference again (reading or writing), we can be sure that this unknown code did
+not access the memory behind our mutable reference at all (or we have UB).  For
+example:
+
+{% highlight rust %}
+fn demo_mut_unique(our: &mut i32) -> i32 {
+  Retag(our); // So we can be sure the tag is unique
+
+  *our = 5;
+
+  unknown_code();
+
+  // We know this will return 5, and moreover if `unknown_code` does not panic
+  // we know we could do the write after calling `unknown_code` (because it
+  // cannot even read from `our`).
+  *our
+}
+{% 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.
+
+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
+have this tag at the top of the (unfrozen) stack.  This is not just the case
+immediately after retagging.  We know our reference is at the top of the stack
+after writing to it, so in the following example we know that `unknown_code_2`
+cannot access `our`:
+
+{% highlight rust %}
+fn demo_mut_advanced_unique(our: &mut u8) -> u8 {
+  Retag(our); // So we can be sure the tag is unique
+
+  unknown_code_1(&*our);
+
+  // This "re-asserts" uniqueness of the reference: After writing, we know
+  // our tag is at the top of the stack.
+  *our = 5;
+
+  unknown_code_2();
+
+  // We know this will return 5
+  *our
+}
+{% endhighlight %}
+
+### 5.2 Shared References (without `UnsafeCell)` are Read-only
+
+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
+our reference if it wants), and then we use the reference again, we know that
+the value pointed to by the reference has not been changed.  For example:
+
+{% highlight rust %}
+fn demo_shr_frozen(our: &u8) -> u8 {
+  Retag(our); // So we can be sure the tag actually carries a timestamp
+
+  // See what's in there.
+  let val = *our;
+  
+  unknown_code(our);
+
+  // We know this will return `val`
+  *our
+}
+{% 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.
+
+One interesting observation here for both of these proofs is that all we rely on
+when the unknown code is executed are the actions performed on every memory
+access.  The additional checks that happen when a pointer is dereferenced only
+matter in *our* code, not in the foreign code.  This indicates that we could see
+the checks on pointer dereference as another "shadow state operation" next to
+`Retag` and `EscapeToRaw`, and then these three operations plus the actions on
+memory accesses are all that there is to Stacked Borrows.  This is difficult to
+implement in miri because dereferences can happen any time a path is evaluated,
+but it is nevertheless interesting and might be useful in a "lower-level MIR"
+that does not permit dereferences in paths.
+
+## 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
+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.
+
+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.
+
+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
+regularly to keep working, so it is not currently on crates.io.  Installation
+instructions for miri are provided
+[in the README](https://github.com/solson/miri/#running-miri).  Please let me
+know if you are having trouble with anything.  You can report issues, comment on
+this post or find me in chat (as of recently, I am partial to Zulip where we
+have an
+[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
+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
+for your case.
+
+Unfortunately, `cargo miri test` is currently broken; if you want to help with
+that [here are some details](https://github.com/solson/miri/issues/479).
+Moreover, wouldn't it be nice if we could run the entire libcore, liballoc and
+libstd test suite in miri?  There are tons of interesting cases of Rust's core
+data structures being exercise there, and the comparatively tiny miri test suite
+has already helped to find two soundness bugs, so there are probably more.  Once
+`cargo miri test` works again, it would be great to find a way to run it on the
+standard library test suites, and set up something so that this happens
+automatically on a regular basis (so that we notice regressions).
+
+As you can see, there is more than enough work for everyone.  Don't be shy!  I
+have a mere three weeks left on this internship, after which I will have to
+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. :)