calrify unfreeze-on-write

[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 54dd417c8aecb7aee373717ca1d1a21b8646f551..f523482baaf25170d33c7de0f2f6bd5367b16247 100644 (file)
--- a/personal/_posts/2018-08-07-stacked-borrows.md
+++ b/personal/_posts/2018-08-07-stacked-borrows.md
@@ -198,7 +198,7 @@ However, I now came to the conclusion that tagging pointers is a price worth pay
 
 I hope you now have a clear idea of the basic structure of the model I am proposing: The stack of borrows, the freeze flag, and references tagged with the time at which they got created.
 The full model is not quite as simple, but it is not much more complicated either.
 
 I hope you now have a clear idea of the basic structure of the model I am proposing: The stack of borrows, the freeze flag, and references tagged with the time at which they got created.
 The full model is not quite as simple, but it is not much more complicated either.

-We need two add just two more concepts: Retagging and barriers.
+We need to add just two more concepts: Retagging and barriers.

 
 ### 4.1 Retagging
 
 
 ### 4.1 Retagging
 


@@ -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))`.
   - 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)`.
   - 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)`.