add GhostCell paper

[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 f523482baaf25170d33c7de0f2f6bd5367b16247..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.
 
+**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 %}