more disucssion of retag redundancy check

[web.git] / personal / _posts / 2018-08-07-stacked-borrows.md

diff --git a/personal/_posts/2018-08-07-stacked-borrows.md b/personal/_posts/2018-08-07-stacked-borrows.md
index 3577e3da0eb8be79dad86bd938cb6ab9ffb44dab..6469a1d8ed0f11164e3dad53219bf00fa91357c5 100644 (file)
--- a/personal/_posts/2018-08-07-stacked-borrows.md
+++ b/personal/_posts/2018-08-07-stacked-borrows.md
@@ -442,7 +442,7 @@ Now we can look at what happens for each operation.
   - Compute `new_bor` from `new_tag` and the type of the reference being created.
   - `reactivate(bor)`.
   - If this is a function argument coming in: `loc.borrows.push(FnBarrier(stack_height))`.
-  - `initiate(new_bor)`. Note that this is a NOP if `new_bor` is already active -- in particular, if the location is frozen and this is a shared reference with interior mutability, we do *not* push anything on top of the barrier. This is important, because we do not want to push that might unfreeze the location when being reactivated.
+  - `initiate(new_bor)`. Note that this is a NOP if `new_bor` is already active -- in particular, if the location is frozen and this is a shared reference with interior mutability, we do *not* push anything on top of the barrier. This is important, because any reactivation that unfreezes this location must lead to UB while the barrier is still present.
   - Change reference tag to `new_tag`.
 * Any time a raw pointer is created from a reference, we might have to do a raw reborrow.
   - `reactivate(bor)`.
@@ -450,6 +450,7 @@ Now we can look at what happens for each operation.
 * Any time a function returns, we have to clean up the barriers.
   - Iterate over all of memory and remove the matching `FnBarrier`. This is where the "stack" becomes a bit of a lie, because we also remove barriers from the middle of a stack.<br>
     This could be optimized by adding an indirection, so we just have to record somewhere that this function call has ended.
+* Any time memory is deallocated, this counts as mutation, so the usual rules for that apply. After that, the stacks of the deallocated bytes must not contain any barriers.
 
 
 If you want to test your own understanding of "Stacked Borrows", I invite you to go back to [Section 2.2 of "Types as Contracts"]({% post_url 2017-07-17-types-as-contracts %}#22-examples) and look at the three examples here.