ralf/_posts/2019-05-21-stacked-borrows-2.1.md

   1 ---
   2 title: "Putting the stack back into Stacked Borrows"
   3 categories: rust research
   4 forum: https://internals.rust-lang.org/t/stacked-borrows-2/9951/8
   5 ---
   6
   7 Less than a month ago, [I announced Stacked Borrows 2]({% post_url 2019-04-30-stacked-borrows-2 %}).
   8 In particular, I hoped that that version would bring us closer to proper support for two-phase borrows.
   9 Turns out I was a bit too optimistic!
  10 Last week, @Manishearth [asked on Zulip](https://rust-lang.zulipchat.com/#narrow/stream/136281-t-lang.2Fwg-unsafe-code-guidelines/topic/safety.20of.20stable.20containers) why Miri rejected a certain program, and it turned out that the issue was related to two-phase borrows: in combination with interior mutability, behavior wasn't always what we wanted it to be.
  11 So, I went back to the drawing board and tried to adjust Stacked Borrows.
  12
  13 In the end, I decided to give up on "proper" support for two-phase borrows for now, which I [explained here](https://github.com/rust-lang/rust/issues/56254#issuecomment-493756649).
  14 But I also made some tweaks to Stacked Borrows that affect all accesses (not just two-phase borrows), and that's what this post is about.
  15 I am referring to this as "Stacked Borrows 2.1".
  16
  17 <!-- MORE -->
  18
  19 ## Stacked Borrows: Table of Contents
  20
  21 Before we start, here's a list of all posts about Stacked Borrows so far.
  22 I am assigning them each a version number to hopefully make it a bit less confusing (I did not exactly foresee an entire series of posts on this subject).
  23
  24 * [Stacked Borrows 0.1]({% post_url 2018-08-07-stacked-borrows %}) is my initial idea of what Stacked Borrows might look like before I started implementing it. This post is interesting for some of the historical context it gives, but is largely superseded by the next post.
  25 * [Stacked Borrows 1.0]({% post_url 2018-11-16-stacked-borrows-implementation %}) is the first version that got implemented. This post is self-contained; I was not happy with some of my explanations in the original post so I decided to give it another shot.
  26 * [Stacked Borrows 1.1]({% post_url 2018-12-26-stacked-borrows-barriers %}) extends Stacked Borrows 1 with partial support for two-phase borrows and explains the idea of "barriers".
  27 * [Stacked Borrows 2.0]({% post_url 2019-04-30-stacked-borrows-2 %}) is a re-design of Stacked Borrows 1 that maintains the original core ideas, but changes the mechanism to support more precise tracking of shared references.  In the following, I will assume you have read at least this post.
  28
  29 ## Is there a stack?
  30
  31 As I [explained the last time]({% post_url 2019-04-30-stacked-borrows-2 %}#why-not-a-strict-stack-discipline), there's not really a "stack" any more in Stacked Borrows.
  32 I showed a widely-used pattern that would be ruled out by a strict stack discipline, and at least the basic optimizations that motivated Stacked Borrows are fine with this weaker model.
  33 But one thing that I realized is that that pattern just shows that *read accesses* cannot strictly maintain a stack.
  34 So maybe write accesses could?
  35
  36 And indeed, that's one of the things that changed with Stacked Borrows 2.1: on a write access, instead of removing just the incompatible items above the granting item, we remove *everything* above (and including) the first incompatible item above the granting item.
  37 Or, if we inline the definition of "compatible":
  38 * When writing to a `Unique` item, we remove everything above (this is unchanged to Stacked Borrows 2.0).
  39 * When writing to a `SharedReadWrite`, we keep the *adjacent* `SharedReadWrite` above it, but then remove *everything* above the first "other" item.
  40
  41 The last point is a change in behavior: the following code used to be legal, and is now UB.
  42 {% highlight rust %}
  43 fn main() { unsafe {
  44     let c = &UnsafeCell::new(UnsafeCell::new(0));
  45     let inner_uniq = &mut *c.get();
  46     // stack: [c: SharedReadWrite, inner_uniq: Unique]
  47
  48     let inner_shr = &*inner_uniq; // adds a SharedReadWrite
  49     // stack: [c: SharedReadWrite, inner_uniq: Unique, inner_shr: SharedReadWrite]
  50
  51     *c.get() = UnsafeCell::new(1); // invalidates inner_shr
  52     // stack: [c: SharedReadWrite]
  53
  54     let _val = *inner_shr.get(); // error because the tag is not on the stack any more
  55 } }
  56 {% endhighlight %}
  57 (I am writing variable names in the stack to refer to those variable's tag.)
  58 In stacked Borrows 2.0, the stack at the end would instead have been `[c: SharedReadWrite, inner_shr: SharedReadWrite]`, thus permitting the final access.
  59
  60 ## Let there be structure!
  61
  62 I am not deeply invested in allowing or forbidding that last example.
  63 However, this change has the nice side-effect that it gives rise to some structure in how the stack looks like and how it can be interpreted, and I think that is helpful when understanding Stacked Borrows.
  64
  65 Remember that the stack consists of items that grant `Unique`, `SharedReadWrite` or `SharedReadOnly` permission.
  66
  67 However, `SharedReadOnly` only occurs at the top of the stack (there can be multiple of these at the top, but there will never be another permission above a `SharedReadOnly`).
  68 For example, the stack might end in `[..., a: Unique, x: SharedReadOnly, y: SharedReadOnly]`.
  69 Here, `x` and `y` are read-only shared references that are currently allowed to access this memory.
  70 They are either derived from `a`, or derived from another one of the read-only shared references.
  71 (I am using the non-transitive version of "derived from" here, i.e., I am talking about the *direct* predecessor.)
  72
  73 Further down in the stack, if we have two neighboring `Unique`, that says that the one further up the stack was "derived from" the one further down.
  74
  75 But what about `SharedReadWrite`?
  76 If we think of an `&mut UnsafeCell<T>` (which will have a `Unique` permission), then each time we create a shared reference from it, that will add a `SharedReadWrite` above the `Unique`.
  77 We might end up with `[..., a: Unique, x: SharedReadWrite, y: SharedReadWrite]`.
  78 Here, `x` and `y` can all be used interchangeably: reading from or writing to any of these `SharedReadWrite` references will not invalidate any of the others!
  79 The way I think about it is that a bunch of adjacent `SharedReadWrite` permissions together form one "block" on the stack.
  80 Writing to the `Unique` from which they all come (`a` in our example) invalidates the entire block.
  81
  82 This is a lot like the "block" of `SharedReadOnly` that may exist at the top of the stack.
  83 Except that, from an `&UnsafeCell<T>` with `SharedReadWrite` permission, we can derive a `&mut T` with `Unique` permission!
  84 So we might have a stack like `[..., a: Unique, x: SharedReadWrite, y: SharedReadWrite, b: Unique]` where `b` is derived from `x` or `y` (we don't know which, but that has no effect on what programs are allowed).
  85 In case of nested `UnsafeCell`, we might even have another (block of) `SharedReadWrite` further up the stack!
  86
  87 So, in general, the stack looks as follows (starting at the bottom):
  88 * First a "stem" consisting of a sequence of "blocks". A "block" in the stem is either a single `Unique` permissions and or a bunch of consecutive `SharedReadWrite` permissions.
  89 * Finally, optionally, a "cap" consisting of a "block" of consecutive `SharedReadOnly` permissions.
  90
  91 For all of these blocks, we have that each pointer in a block is derived either from a pointer in the next block down the stack, or another pointer in the same block.
  92
  93 In this framework, we can re-cast the new rule for write access as: when writing to a pointer in some block, remove all blocks further up the stack.
  94
  95 ## But what about reads?
  96
  97 However, it turns out that the old rule for read accesses wrecks havoc with this block-based intuition that I just described.
  98 Remember that on a read, we removed all read-incompatible items above the granting item---which, when inlining the definition of "compatibility", means removing all `Unique` above the granting item.
  99 If this `Unique` item sits between two (blocks of) `SharedReadWrite` items, that has the unfortunate side-effect of *merging* these two blocks!
 100
 101 For example, prior to the read access, we might have had a stack like `[x: SharedReadWrite, a: Unique, y: SharedReadWrite]`. In this situation, writing to `x` would (under the new rules) invalidate `y` because it is in a block further up the stack.
 102 However, after reading from `x`, the stack changes to `[x: SharedReadWrite, y: SharedReadWrite]`.
 103 The two blocks got merged into one, and now `x` and `y` can be used interchangeably!
 104 That seems like a strange effect.
 105 Furthermore, this breaks the invariant that in a block of `SharedReadWrite`, each pointer is derived from another pointer in the same block or in the next block down the stack: `y` is derived from `a`, not from `x`!
 106
 107 To fix this and make sure that the structure I described in the previous section actually holds, I changed read accesses to avoid merging two blocks of `SharedReadWrite`.
 108 Instead of just removing `Unique`, we replace them by a `Disabled` "permission" that grants no access, but just serves to separate two blocks.
 109 With that, the stack in our example becomes `[x: SharedReadWrite, a: Disabled, y: SharedReadWrite]`.
 110 This keeps the two (singleton) blocks of `SharedReadWrite` apart, so even after reading from `x`, a subsequent write to `x` will still invalidate `y`.
 111
 112 ## Conclusion
 113
 114 That's it already.
 115 You can find a complete description (but without explanation) of Stacked Borrows 2.1 [in the UCG repository](https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/stacked-borrows.md).
 116
 117 I mostly wanted to talk about this structure of "blocks" that still looks very much like a stack, just a more refined version of what we had in Stacked Borrows 1.
 118 Back then, such a block of `SharedReadWrite` was basically represented by a single `Raw` item, not differentiating *which* pointers are allowed to access the memory in this way.
 119 Similarly, the block of `SharedReadOnly` was represented by the "freeze" flag, which excluded some shared references but was still not very precise in encoding which pointers are allowed to read.
 120 The key contribution of Stacked Borrows 2, then, was to refine these rather coarse notions and keep track exactly of which shared references are part of which block.
 121
 122 For the future, it will be interesting to figure out if we can track raw pointers the same way we are now tracking shared references with interior mutability, or if that will rule out too much existing code.
 123 I don't really have a timeline for this problem though, the next immediate steps involve writing a paper about Stacked Borrows and then writing a PhD thesis about... lots of stuff. ;)