but we have to accept that there might be active mutable references assuming
exclusive access to the same locations. That on its own is not enough, though.
-I also added a special exception: When "creating a raw reference"
-(`EscapeToRaw`, or `Retag` on a shared reference when we are inside an
-`UnsafeCell`), we still first check that the pointer this reference is created
-one is allowed to be dereferenced -- and we remember the position of the item on
-the stack that justifies this, let's call this `ptr_idx`. Remember, that does
-not change the stack, so it has no adverse effect in `demo_refcell`. Next, we do
-a very peculiar check:
-
-1. Determine if the new reference we are creating (it will have a `Shr` tag) is
- *already dereferencable*. This is possible, for example, if the location
- already got shared previously. This is also the case in `demo_refcell`:
- Creating `rc_shr` pushed a `Shr` onto the stack. We again remember the
- position of the item that justifies this, let's call it `new_idx`.
-
- - If this is the case, we moreover *compare* the `new_idx` and `ptr_idx`.
- If `new_idx` is *above* `ptr_idx` on the stack, that means that not only
- is the location already being shared (so we can dereference with our new
- `Shr` tag), moreover *the pointer we create this reference from has
- already been shared*. The new pointer is already "derived from" the one
- this reference is based on. Basically, everything that we wanted to do
- while creating this reference has already happened. In this case, we just
- do nothing else: We leave the stacks unchanged.
-
- - Otherwise, we continue as usual.
-
-This rule has the effect that in our example above, when we create `shr_ref`, we
-do not pop `Uniq(2)` off the stack, and hence the access through `mut_ref` at
-the end remains valid.
-
-This may sound like a weird special case, and it is. I would surely not have
-thought of this if `RefCell` would not force our hands here. However, it also
-does not seem to break any of the important properties of the model (mutable
-references being unique and shared references being read-only except for
-`UnsafeCell`).
+I also added a new check to the retagging procedure: Before taking any action
+(i.e., before step 3, which could pop items off the stack), we check if the
+reborrow is redundant: If the new reference we want to create is already
+dereferencable (because it item is already on the stack and, if applicable, the
+stack is already frozen), *and* if the item that justifies this is moreover
+"derived from" the item that corresponds to the old reference, then we just do
+nothing. Here, "derived from" means "further up the stack". Basically, the
+reborrow has already happened and the new reference is ready for use, and
+(because of that "derived from" check), we know that using the new reference
+will *not* pop the item corresponding to the old reference off the stack. In
+that case, we avoid popping anything, to keep other references valid.
+
+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.
+
+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`).
## 4 Differences to the Original Proposal
{% endhighlight %}
The proof sketch goes as follows: After retagging the reference, we know it is
-at the top of the stack and the location is not frozen. For any access
-performed by the unknown code, we know that access cannot use the tag of our
-reference because the tags are unique and not forgeable. Hence if the unknown
-code accesses our locations, that would pop our tag from the stack. When we use
-our reference again, we know it is on the stack, and hence has not been popped
-off. Thus there cannot have been an access from the unknown code.
+at the top of the stack and the location is not frozen. (The "redundant
+reborrow" rule does not apply because a fresh `Uniq` tag can never be
+redundant.) For any access performed by the unknown code, we know that access
+cannot use the tag of our reference because the tags are unique and not
+forgeable. Hence if the unknown code accesses our locations, that would pop our
+tag from the stack. When we use our reference again, we know it is on the
+stack, and hence has not been popped off. Thus there cannot have been an access
+from the unknown code.
Actually this theorem applies *any time* we have a reference whose tag we can be
sure has not been leaked to anyone else, and which points to locations which
{% endhighlight %}
The proof sketch goes as follows: After retagging the reference, we know the
-location is frozen. If the unknown code does any write, we know this will
-unfreeze the location. The location might get re-frozen, but only at the
-then-current timestamp. When we do our read after coming back from the unknown
-code, this checks that the location is frozen *at least* since the timestamp
-given in its tag, so if the location is unfrozen or got re-frozen by the unknown
-code, the check would fail. Thus the unknown code cannot have written to the
-location.
+location is frozen (this is the case even if the "redundant reborrow" rule
+applies). If the unknown code does any write, we know this will unfreeze the
+location. The location might get re-frozen, but only at the then-current
+timestamp. When we do our read after coming back from the unknown code, this
+checks that the location is frozen *at least* since the timestamp given in its
+tag, so if the location is unfrozen or got re-frozen by the unknown code, the
+check would fail. Thus the unknown code cannot have written to the location.
One interesting observation here for both of these proofs is that all we rely on
when the unknown code is executed are the actions performed on every memory
projects / web.git / blobdiff