add my PhD thesis

[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..7397780b0edb87210813671bc800b0ebc3d54be6 100644 (file)
--- a/personal/_posts/2018-08-07-stacked-borrows.md
+++ b/personal/_posts/2018-08-07-stacked-borrows.md
@@ -15,6 +15,12 @@ The model I am proposing here is by far not the first attempt at giving a defini
 But before I delve into my latest proposal, I want to briefly discuss a key difference between my previous model and this one:
 "Types as Contracts" was a fully "validity"-based model, while "Stacked Borrows" is (to some extent) "access"-based.
 
+**Update:**
+Since publishing this post, I have written [another]({% post_url 2018-11-16-stacked-borrows-implementation %}) blog post about a slightly adjusted version of Stacked Borrows (the first version that actually got implemented).
+That other post is self-contained, so if you are just interested in the current state of Stacked Borrows, I suggest you go there.
+Only go on reading here if you want some additional historic context.
+**/Update**
+
 ## 1 Validity-based vs. Access-based
 
 An "access"-based model is one where certain properties -- in this case, mutable references being unique and shared references pointing to read-only memory -- are only enforced when the reference is actually used to *access* memory.
@@ -135,7 +141,7 @@ fn demo3(x: &mut i32) -> i32 {
   let y = unsafe { & *raw }; // Now memory gets frozen (recording the timestamp)
   let _val = *y; // Okay because memory was frozen since `y` was created
   *x = 3; // This "reactivates" `x` by unfreezing and popping the stack.
-  let z = unsafe { & *raw }; // Now memory gets frozen *again*
+  let z = &*x; // Now memory gets frozen *again*
   *y // This is UB! Memory has been frozen strictly after `y` got created.
 }
 {% endhighlight %}
@@ -198,7 +204,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.
-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
 
@@ -442,7 +448,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)`.