From: Ralf Jung Date: Thu, 13 Dec 2018 18:33:10 +0000 (+0100) Subject: fix a bug, link to new post X-Git-Url: https://git.ralfj.de/web.git/commitdiff_plain/160d9782437e9868c58bdc1f219940dc916535bb?ds=sidebyside fix a bug, link to new post --- diff --git a/ralf/_posts/2018-08-07-stacked-borrows.md b/ralf/_posts/2018-08-07-stacked-borrows.md index f523482..0f36e05 100644 --- 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 %}