feedback from Niko

diff --git a/personal/_drafts/stacked-borrows-implementation.md b/personal/_drafts/stacked-borrows-implementation.md
index 5d7a7e70364a30488879f46a70902dede9285bc6..ac3624da458cb6f07dcbdef4773b8d483fd8f327 100644 (file)
--- a/personal/_drafts/stacked-borrows-implementation.md
+++ b/personal/_drafts/stacked-borrows-implementation.md
@@ -65,7 +65,7 @@ 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.
 
 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
 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


@@ -159,8 +159,8 @@ have to improve that one):
 
 ## 2 Enabling Sharing
 
 
 ## 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.
 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.


@@ -341,18 +341,19 @@ 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).
 
 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
 
 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
 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
     - 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


@@ -364,17 +365,20 @@ The following checks are done on every pointer dereference:
 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
 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`).
 
 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.
 
 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
 
 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


@@ -403,7 +407,7 @@ 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"
 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
 Unfortunately, things are not so easy.
 
 The uniqueness of mutable references entirely rests on the fact that the pointer


@@ -440,7 +444,7 @@ 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
 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 descend is already implemented, but the
+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.)  However, we do *not* descend recursively
 through references: Retagging a `&mut &mut u8` will only retag the *outer*
 reference.


@@ -457,7 +461,7 @@ fn demo0() {
   // stack: [Uniq(0)]; not frozen
   
   let y = &mut *x;
   // 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.
   // stack: [Uniq(0), Uniq(1)]; not frozen
 
   // Check that `Uniq(1)` is on the stack, then pop to bring it to the top.


@@ -474,7 +478,8 @@ fn demo0() {
 {% endhighlight %}
 
 For each reference, `Retag` does the following (we will slightly refine these
 {% endhighlight %}
 
 For each reference, `Retag` does the following (we will slightly refine these

-instructions later):
+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 a mutable reference and `Shr(Some(_))` for
    a shared reference.


@@ -503,7 +508,7 @@ 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
+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):
 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):


@@ -607,7 +612,7 @@ 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
 reborrow is redundant: If the new reference we want to create is already
 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 it item is already on the stack and, if applicable, the
+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
 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


@@ -616,23 +621,27 @@ reborrow has already happened and the new reference is ready for use, and
 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.
 
 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.
 

-This rule applies in our example above when we create `shr_ref` from `mut_ref`.
-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.
+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 read-only
 except for `UnsafeCell`).  Moreover, when pushing an item to the stack (at the
 
 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 read-only
 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
-was frozen, the reborrow would be redundant.
+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
 
 With this extension, the instructions for retagging and `EscapeToRaw` now look

-as follows:
+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 a mutable reference, `Shr(Some(_))` for a
    shared reference, `Shr(None)` if this is `EscapeToRaw`.


@@ -677,7 +686,7 @@ 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
 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
 (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


@@ -877,3 +886,6 @@ 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. :)
 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](). -->