fix example

diff --git a/ralf/_posts/2019-04-30-stacked-borrows-2.md b/ralf/_posts/2019-04-30-stacked-borrows-2.md
index c57098c4aa7d977ac85fdc2b4be20d1542fce5b3..dec44ed4fa1cc1f49b9184ffd11db8e2c19e2181 100644 (file)
--- a/ralf/_posts/2019-04-30-stacked-borrows-2.md
+++ b/ralf/_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;
 
 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.
 }
 {% 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
 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!
     // 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.
 }
 {% 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.)
 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!
 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.
 
 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.