X-Git-Url: https://git.ralfj.de/web.git/blobdiff_plain/9bfe062e102ffeb1ec5f1b159f625bebf1ad0349..11eff2ea5dd6029346c369aaec53dbb68445c9f8:/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 c57098c..5b2abb0 100644
--- a/personal/_posts/2019-04-30-stacked-borrows-2.md
+++ b/personal/_posts/2019-04-30-stacked-borrows-2.md
@@ -16,7 +16,7 @@ Before we start, let me give a brief overview over the posts on Stacked Borrows
 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 best post to start with, if you are catching up.
+* [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
@@ -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!
+    _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.