uninit post: add forward link to provenance post

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

diff --git a/ralf/_posts/2018-08-07-stacked-borrows.md b/ralf/_posts/2018-08-07-stacked-borrows.md
index 6469a1d8ed0f11164e3dad53219bf00fa91357c5..7397780b0edb87210813671bc800b0ebc3d54be6 100644 (file)
--- a/ralf/_posts/2018-08-07-stacked-borrows.md
+++ b/ralf/_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.
 
 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.
 ## 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 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 %}
   *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.
 
 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