X-Git-Url: https://git.ralfj.de/web.git/blobdiff_plain/9b34d4585d4f6db027cce07268ecda3b9da65491..1f0413b8b626f2b69ec468a119603daa67656ab1:/personal/_posts/2019-04-30-stacked-borrows-2.md?ds=inline diff --git a/personal/_posts/2019-04-30-stacked-borrows-2.md b/personal/_posts/2019-04-30-stacked-borrows-2.md index 7951899..669d49d 100644 --- a/personal/_posts/2019-04-30-stacked-borrows-2.md +++ b/personal/_posts/2019-04-30-stacked-borrows-2.md @@ -10,10 +10,19 @@ I assume some familiarity with the prior version and will not explain everything +## Stacked Borrows: Table of Contents + +Before we start, let me give a brief overview over the posts on Stacked Borrows that I have written so far. +I didn't plan this out in advance, so things are a bit more messy than I would like. + +* [Stacked Borrows: An Aliasing Model For Rust]({% post_url 2018-08-07-stacked-borrows %}) is the first post of the series and describes my initial ideas of what Stacked Borrows would look like before I started implementing them. It might be interesting for some of the context it gives, but is largely superseded by the next post. +* [Stacked Borrows Implemented]({% post_url 2018-11-16-stacked-borrows-implementation %}) describes Stacked Borrows 1 and my experience implementing it. It is self-contained; I was not happy with some of my explanations in the original post so I decided to give it another shot. **This is the post to read if you are catching up.** +* [Barriers and Two-phase Borrows in Stacked Borrows]({% post_url 2018-12-26-stacked-borrows-barriers %}) describes how I extended Stacked Borrows 1 with partial support for two-phase borrows and explains the idea of "barriers". You do not have to have read that post to understand Stacked Borrows 2, except for the parts that specifically refer to barriers and two-phase borrows. + ## The problem -The problem I wanted to solve was that the first version of Stacked Borrows only performed very little tracking of shared references. -My thinking was, if the location is read-only anyway, then it does not harm to grant anyone read access. +The problem I wanted to solve with Stacked Borrows 2 was that the first version of Stacked Borrows only performed very little tracking of shared references. +My thinking was, if the location is read-only anyway, then it is not harmful to grant anyone read access. However, [as @arielby noted](https://github.com/rust-lang/unsafe-code-guidelines/issues/87), this leads to loss of optimization potential in cases where a function receives a mutable reference (which is supposed to have no aliases) and then creates a shared reference from it: {% highlight rust %} fn main() { @@ -24,15 +33,17 @@ fn main() { fn foo(a: &mut u32, y: *mut u32) -> u32 { *a = 1; - let _b = &*a; // This freezes `x`. Frozen locations can be read by any raw pointer. - unsafe { *y = 2; } // Hence, this legal in Stacked Borrows. - return *a; // But we want to optimize this to always return 1! + let _b = &*a; // This freezes `*a`. Frozen locations can be read by any raw pointer. + let _val = unsafe { *y; }; // Hence, this legal in Stacked Borrows. + *a = 2; // But we might want to drop the earlier `*a = 1` because it gets overwritten! + _val } {% endhighlight %} Stacked Borrows 1 allowed any raw pointer to read a frozen location. Basically, once a location is frozen we do not keep track of which pointer is allowed to read; we just allow all pointers to read. -However, that means that `&*a` above (reborrowing a mutable reference as a shared reference) has the unintended side-effect of permitting raw pointers to access `*a`! -This violates the idea that `a` is a unique pointer: we'd like to assume that `foo` can only ever return `1`, because `y` cannot possibly alias with `a`. +However, that means that `&*a` above (reborrowing a mutable reference as a shared reference) has the unintended side-effect of permitting raw pointers to read `*a`! +This violates the idea that `a` is a unique pointer: we'd like to remove the first write (`*a = 1`) because it gets overwritten later and there is no read *through `a`* in the mean time. +The issue is, there *is* an aliasing read through `y`, so removing the seemingly redundant write would change the return value of `foo` from `1` to `0`. Hence calling `foo` like we do here with `a` and `y` pointing to the same thing must be undefined behavior---and yet, Stacked Borrows 1 considered the example above to be legal. ## The solution @@ -69,7 +80,7 @@ pub struct Stack { {% endhighlight %} The *tag* is also simpler than it was before: there are no longer separate tags for mutable and shared references. {% highlight rust %} -pub type PtrId = NonZeroU64; +pub type PtrId = u64; pub enum Tag { Tagged(PtrId), Untagged, @@ -88,6 +99,7 @@ For each affected location, we go through two steps: first we try to find the *g **Finding the granting item.** To find the granting item, we traverse the borrow stack top-to-bottom and search for an item that has the same tag. If this is a write access, we go on looking until we find an item with the right tag whose permission is `SharedReadWrite` or `Unique`---we do not consider items with `SharedReadOnly` permission to grant a write access. +This is the item that grants pointers tagged `tag` the permission to perform the given access, hence the name (the same concept used to be called "matching item" in Stacked Borrows 1). Once we found the granting item, we remember its position in the stack; that will be important for the second step. If no granting item can be found, the access causes undefined behavior. @@ -188,14 +200,16 @@ fn foo(a: &mut u32, y: *mut u32) -> u32 { // Stack: [ (0: Unique), (1: Unique), (2: SharedReadOnly) ] // UB: y is Untagged, and there is no granting item in the stack! - unsafe { *y = 2; } + let _val = unsafe { *y }; + + *a = 2; - return *a; + _val } {% endhighlight %} Initially, `x` with tag `Tagged(0)` is the only reference, and the stack says that this is the only pointer with any kind of permission. Next, we cast `x` to a raw pointer. -The raw retagging of `p` turns `p` into an `Untagged` pointer, and adds a new item granting thusly tagged pointers `SharedReadWrite` permission. +The raw retagging of `p` turns `p` into an `Untagged` pointer, and adds a new item granting `Untagged` pointers `SharedReadWrite` permission. (Really, in the MIR it will say `&mut *x as *mut u32`, so there will be an additional `Unique` permission for the temporary mutable reference, but that makes no difference and I hope [we will change that eventually](https://github.com/rust-lang/rfcs/pull/2582).) Then `foo` gets called, which starts with the usual retagging of all reference arguments. @@ -206,9 +220,9 @@ Nothing interesting happens when writing to `a`. When `_b` gets created, it gets assigned the new tag `Tagged(2)`, and a new item `2: SharedReadOnly` is pushed to the stack. As we can see, shared and mutable references no longer differ in the tag they carry; the only difference is what kind of permission they get granted. (I think this is a nice improvement from Stacked Borrows 1, where shared references had a different kind of tag. In particular, transmutes between mutable references and shared pointers no longer need any kind of special treatment.) -Finally, we come to the interesting point: the program writes to `y`. +Finally, we come to the interesting point: the program reads from `y`. That pointer is `Untagged`, and there is no item granting any access to such pointers, and thus the access is UB! -This is in contrast to Stacked Borrows 1, where instead of `2: SharedReadOnly` we set a special "frozen" marker on this location that would, as a side-effect, also grant untagged pointers read-only access. +This is in contrast to Stacked Borrows 1, where instead of `2: SharedReadOnly` we set a special "frozen" marker on this location that would, as a side-effect, also grant untagged pointers like `y` read-only access. In general, during retagging, we start with some original tag used by our "parent" pointer, and we have a fresh tag `N` that will be used for the new pointer. We have to decide which permission to grant so this tag, and where in the "stack" to insert it.