X-Git-Url: https://git.ralfj.de/web.git/blobdiff_plain/62638a04ca1a70a8b5cc9ced836113624ae6ae0e..ce79f527e9ae2a9b9422367f538118ed87fb2a7d:/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..37cdf50 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 @@ -147,7 +147,7 @@ Shared references with interior mutability do not really have any restrictions i For every location in memory, we keep track of a stack of borrows (`Uniq(_)` or `Raw`), and potentially "top off" this stack by freezing the location. A frozen location is never written to, and no `Uniq` is pushed. -Whenever a mutable reference is created, a matching `Uniq` is pushed onto the stack for every location "covered by" the reference -- i.e., the locations that would be accessed when the reference is used (starting at where it points to, and going on for `mem::size_of::` many bytes). +Whenever a mutable reference is created, a matching `Uniq` is pushed onto the stack for every location "covered by" the reference -- i.e., the locations that would be accessed when the reference is used (starting at where it points to, and going on for `size_of_val` many bytes). Whenever a shared reference is created, if there is no interior mutability, we freeze the locations if they are not already frozen. If there is interior mutability, we just push a `Raw`. Whenever a raw pointer is created from a mutable reference, we push a `Raw`. @@ -169,7 +169,7 @@ In particular, notice that `x` and `y` in the first example have the same addres If we compared them as raw pointers, they would turn out equal. And yet, it makes a huge difference if we use `x` or `y`! -If you read my previous post on [why pointers are complicated](2018-07-24-pointers-and-bytes), this should not come as too much of a surprise. +If you read my previous post on [why pointers are complicated]({% post_url 2018-07-24-pointers-and-bytes %}), this should not come as too much of a surprise. There is more to a pointer, or a reference (I am using these terms mostly interchangeably), than the address in memory that it points to. For the purpose of this model, we assume that a value of reference type consists of two parts: An address in memory, and a tag used to store the time when the reference was created. @@ -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 @@ -239,7 +239,7 @@ It is also needed to explain why we can put the [`noalias` parameter attribute]( Consider the following code: {% highlight rust %} -fn demo5(x: &mut i32, y: usize) -> i32 { +fn demo5(x: &mut i32, y: usize) { *x = 42; foo(y); } @@ -336,8 +336,11 @@ impl MemoryByte { self.frz_since.map_or(false, |loc_t| loc_t <= acc_t), Mut(acc_m) => // Raw pointers are fine with frozen locations. This is important because &Cell is raw! - (acc_m.is_raw() && self.frozen_since.is_some()) || - self.borrows.last().map_or(false, |loc_itm| loc_itm == Mut(acc_m)), + if self.frozen_since.is_some() { + acc_m.is_raw() + } else { + self.borrows.last().map_or(false, |loc_itm| loc_itm == Mut(acc_m)) + } } }