X-Git-Url: https://git.ralfj.de/web.git/blobdiff_plain/722c8001d506ec4b884bf1679f26268e373998da..99e64258f081e83a64b093725fa6796016f0bffd:/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 f523482..7397780 100644 --- 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 %}