more disucssion of retag redundancy check

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

-Stacked Borrows, you can skip most of this post and go right to
-[section 4](#4-differences-to-the-original-proposal).  If you only want to know
-how to help, jump to [section 6](#6-evaluation-and-how-you-can-help).
+Stacked Borrows, you can skip most of this post and go right to [section 4].  If
+you only want to know how to help, jump to [section 6].

 
 ## 1 Enforcing Uniqueness
 
 
 ## 1 Enforcing Uniqueness
 


@@ -325,6 +324,7 @@ fn demo2() {
 {% endhighlight %}
 
 ### 2.2 Dereferencing a Pointer
 {% endhighlight %}
 
 ### 2.2 Dereferencing a Pointer

+[section 2.2]: #22-dereferencing-a-pointer

 
 As we have seen, we consider the tag of a pointer already when dereferencing it,
 before any memory access happens.  The operation on a dereference never mutates
 
 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


@@ -359,6 +359,7 @@ The following checks are done on every pointer dereference:
       their stack (same check as if the tag had no timestamp).
 
 ### 2.3 Accessing Memory
       their stack (same check as if the tag had no timestamp).
 
 ### 2.3 Accessing Memory

+[section 2.3]: #23-accessing-memory

 
 On an actual memory access, we know the tag of the pointer that was used to
 access (unless it was a raw pointer, in which case the tag we see is
 
 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


@@ -472,8 +473,8 @@ fn demo0() {
 }
 {% endhighlight %}
 
 }
 {% endhighlight %}
 

-For each reference, `Retag` does the following (with one special exception that
-will be explained later):
+For each reference, `Retag` does the following (we will slightly refine these
+instructions later):

 
 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.


@@ -492,6 +493,9 @@ will be explained later):
       2. If the location is outside of `UnsafeCell`, it gets frozen with the
          timestamp of the new reference.
 
       2. If the location is outside of `UnsafeCell`, it gets frozen with the
          timestamp of the new reference.
 

+One high-level way to think about retagging is that it computes a fresh tag, and
+then performs a reborrow of the old reference with the new tag.
+

 ### 3.2 When Pointers Escape
 
 Creating a shared reference is not the only way to share a location: We can also
 ### 3.2 When Pointers Escape
 
 Creating a shared reference is not the only way to share a location: We can also


@@ -621,11 +625,42 @@ nothing, keeping the `Uniq(2)` on the stack, such that the access through
 
 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
 
 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](#5-key-properties), 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`).
+[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.
+
+With this extension, the instructions for retagging and `EscapeToRaw` now look
+as follows:
+
+1. Compute a fresh tag: `Uniq(_)` for a mutable reference, `Shr(Some(_))` for a
+   shared reference, `Shr(None)` if this is `EscapeToRaw`.
+2. Perform the checks that would also happen when we dereference this reference.
+   Remember the position of the item matching the tag in the stack.
+3. Redundancy check: If the new tag passes the checks performed on a
+   dereference, and if the item that makes this check succeed is *above* the one
+   we remembered in step 2 (where the "frozen" state is considered above every
+   item in the stack), then we stop.  We are done for this location.
+4. Perform the actions that would also happen when an actual access happens
+   through this reference (for shared references a read access, for mutable
+   references a write access).
+   Now the location cannot be frozen any more: If the fresh tag is `Uniq`, we
+   just unfroze, if the fresh tag is `Shr` and the location was already frozen
+   then the redundancy check (step 3) would have kicked in.
+5. If the new tag is `Uniq`, push it onto the stack.
+6. If the new tag is `Shr`, push a `Shr` item to the stack.  Then, if the
+   location is outside of `UnsafeCell`, it gets frozen with the timestamp of the
+   new reference.
+
+The one thing I find slightly unsatisfying about the redundancy check is that it
+seems to overlap a bit with the rule that on a *read* access, a `Shr` item
+matches a `Uniq` tag.  Both of these together enable the read-only use of
+mutable references that have already been shared; I would prefer to have a
+single condition enabling that instead of two working together.

 
 ## 4 Differences to the Original Proposal
 
 ## 4 Differences to the Original Proposal

+[section 4]: #4-differences-to-the-original-proposal

 
 The key differences to the original proposal is that the check performed on a
 dereference, and the check performed on an access, are not the same check.  This
 
 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


@@ -633,7 +668,10 @@ 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
 need a weird special exception for `demo1` any more like the original proposal
 did.  The main reason for this, however, is that on an access, we just do not
 know if we are inside an `UnsafeCell` or not, so we cannot do all the checks we

-would like to do.
+would like to do.  Accordingly, I also rearranged terminology a bit.  There is
+no longer one "reactivation" action, instead there is a "deref" check and an
+"access" action, as described above in sections [2.2][section 2.2] and
+[2.3][section 2.3].

 
 Beyond that, I made the behavior of shared references and raw pointers more
 uniform.  This helped to fix test failures around `iter_mut` on slices, which
 
 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


@@ -668,13 +706,15 @@ 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.)
 
 guarantees for it.  (This is another example of a coincidental fix, where I had
 a surprisingly passing test case and then investigated what happened.)
 

-And finally, there is this special exception about creating raw references, to
-fix `demo_refcell`.
+The redundancy check during retagging can be seen as refining a similar check
+that the original model did whenever a new reference was created (where we
+wouldn't change the state if the new borrow is already active).

 
 Finally, the notion of "function barriers" from the original Stacked Borrows has
 not been implemented yet.  This is the next item on my todo list.
 
 ## 5 Key Properties
 
 Finally, the notion of "function barriers" from the original Stacked Borrows has
 not been implemented yet.  This is the next item on my todo list.
 
 ## 5 Key Properties

+[section 5]: #5-key-properties

 
 Let us look at the two key properties that I set out as design goals, and see
 how the model guarantees that they hold true in all valid (UB-free) executions.
 
 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.


@@ -779,13 +819,14 @@ 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
 that does not permit dereferences in paths.
 
 ## 6 Evaluation, and How You Can Help

+[section 6]: #6-evaluation-and-how-you-can-help

 
 I have implemented both the validity invariant and the model as described above
 in miri. This [uncovered](https://github.com/rust-lang/rust/issues/54908) two
 [issues](https://github.com/rust-lang/rust/issues/54957) in the standard
 library, but both were related to validity invariants, not Stacked Borrows.
 With these exceptions, the model passes the entire test suite.  There were some
 
 I have implemented both the validity invariant and the model as described above
 in miri. This [uncovered](https://github.com/rust-lang/rust/issues/54908) two
 [issues](https://github.com/rust-lang/rust/issues/54957) in the standard
 library, but both were related to validity invariants, not Stacked Borrows.
 With these exceptions, the model passes the entire test suite.  There were some

-more test failures in earlier versions (as mentioned in section 4), but the
+more test failures in earlier versions (as mentioned in [section 4]), but the

 final model accepts all the code covered by miri's test suite.  Moreover I wrote
 a bunch of compile-fail tests to make sure the model catches various violations
 of the key properties it should ensure.
 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.