X-Git-Url: https://git.ralfj.de/web.git/blobdiff_plain/62638a04ca1a70a8b5cc9ced836113624ae6ae0e..2c516ac04884d6450a82a8e44cc6146498876597:/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 fd2880a..0314fbb 100644 --- a/ralf/_posts/2018-08-07-stacked-borrows.md +++ b/ralf/_posts/2018-08-07-stacked-borrows.md @@ -13,7 +13,7 @@ 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 extend) "access"-based. +"Types as Contracts" was a fully "validity"-based model, while "Stacked Borrows" is (to some extent) "access"-based. ## 1 Validity-based vs. Access-based @@ -229,7 +229,7 @@ With this additional step, it is now easy to argue that `demo4` above is UB when After using `x`, we know it is active. Next we use and activate `y`, which has to pop `Uniq(x)` as they have distinct tags. Finally, we use `x` again even though it is no longer in the stack, triggering UB. -(A `Uniq` is only veer pushed when it is created, so it is never in the stack more than once.) +(A `Uniq` is only ever pushed when it is created, so it is never in the stack more than once.) ### 4.2 Barriers