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;
-    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.