From e72625e939ac8691bd2e74e9341cc060d76b7acb Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Thu, 2 May 2019 12:59:35 +0200 Subject: [PATCH] fix example --- .../_posts/2019-04-30-stacked-borrows-2.md | 22 +++++++++++-------- 1 file changed, 13 insertions(+), 9 deletions(-) diff --git a/personal/_posts/2019-04-30-stacked-borrows-2.md b/personal/_posts/2019-04-30-stacked-borrows-2.md index c57098c..dec44ed 100644 --- a/personal/_posts/2019-04-30-stacked-borrows-2.md +++ b/personal/_posts/2019-04-30-stacked-borrows-2.md @@ -33,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 by this! + _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 @@ -198,9 +200,11 @@ 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 }; - return *a; + *a = 2; + + _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. @@ -216,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. -- 2.30.2