add firejail 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..0f36e05d5f9fe6a537ebebac4078204236fc1fd9 100644 (file)
--- a/ralf/_posts/2018-08-07-stacked-borrows.md
+++ b/ralf/_posts/2018-08-07-stacked-borrows.md
@@ -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 %}
@@ -198,7 +203,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