fix a bug, link to new post
authorRalf Jung <post@ralfj.de>
Thu, 13 Dec 2018 18:33:10 +0000 (19:33 +0100)
committerRalf Jung <post@ralfj.de>
Thu, 13 Dec 2018 18:33:10 +0000 (19:33 +0100)
ralf/_posts/2018-08-07-stacked-borrows.md

index f523482..0f36e05 100644 (file)
@@ -15,6 +15,11 @@ 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.
+**/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 +140,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 %}