May 21, 2019 • Research, Rust • Edits • Permalink

Putting the stack back into Stacked Borrows

Less than a month ago, I announced Stacked Borrows 2. In particular, I hoped that that version would bring us closer to proper support for two-phase borrows. Turns out I was a bit too optimistic! Last week, @Manishearth asked on Zulip 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. So, I went back to the drawing board and tried to adjust Stacked Borrows.

In the end, I decided to give up on “proper” support for two-phase borrows for now, which I explained here. 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. I am referring to this as “Stacked Borrows 2.1”.

Stacked Borrows: Table of Contents

Before we start, here’s a list of all posts about Stacked Borrows so far. 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).

Is there a stack?

As I explained the last time, there’s not really a “stack” any more in Stacked Borrows. 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. But one thing that I realized is that that pattern just shows that read accesses cannot strictly maintain a stack. So maybe write accesses could?

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. Or, if we inline the definition of “compatible”:

The last point is a change in behavior: the following code used to be legal, and is now UB.

fn main() { unsafe {
    let c = &UnsafeCell::new(UnsafeCell::new(0));
    let inner_uniq = &mut *c.get();
    // stack: [c: SharedReadWrite, inner_uniq: Unique]

    let inner_shr = &*inner_uniq; // adds a SharedReadWrite
    // stack: [c: SharedReadWrite, inner_uniq: Unique, inner_shr: SharedReadWrite]

    *c.get() = UnsafeCell::new(1); // invalidates inner_shr
    // stack: [c: SharedReadWrite]

    let _val = *inner_shr.get(); // error because the tag is not on the stack any more
} }

(I am writing variable names in the stack to refer to those variable’s tag.) In stacked Borrows 2.0, the stack at the end would instead have been [c: SharedReadWrite, inner_shr: SharedReadWrite], thus permitting the final access.

Let there be structure!

I am not deeply invested in allowing or forbidding that last example. 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.

Remember that the stack consists of items that grant Unique, SharedReadWrite or SharedReadOnly permission.

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). For example, the stack might end in [..., a: Unique, x: SharedReadOnly, y: SharedReadOnly]. Here, x and y are read-only shared references that are currently allowed to access this memory. They are either derived from a, or derived from another one of the read-only shared references. (I am using the non-transitive version of “derived from” here, i.e., I am talking about the direct predecessor.)

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.

But what about SharedReadWrite? 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. We might end up with [..., a: Unique, x: SharedReadWrite, y: SharedReadWrite]. 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! The way I think about it is that a bunch of adjacent SharedReadWrite permissions together form one “block” on the stack. Writing to the Unique from which they all come (a in our example) invalidates the entire block.

This is a lot like the “block” of SharedReadOnly that may exist at the top of the stack. Except that, from an &UnsafeCell<T> with SharedReadWrite permission, we can derive a &mut T with Unique permission! 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). In case of nested UnsafeCell, we might even have another (block of) SharedReadWrite further up the stack!

So, in general, the stack looks as follows (starting at the bottom):

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.

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.

But what about reads?

However, it turns out that the old rule for read accesses wrecks havoc with this block-based intuition that I just described. 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. If this Unique item sits between two (blocks of) SharedReadWrite items, that has the unfortunate side-effect of merging these two blocks!

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. However, after reading from x, the stack changes to [x: SharedReadWrite, y: SharedReadWrite]. The two blocks got merged into one, and now x and y can be used interchangeably! That seems like a strange effect. 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!

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. Instead of just removing Unique, we replace them by a Disabled “permission” that grants no access, but just serves to separate two blocks. With that, the stack in our example becomes [x: SharedReadWrite, a: Disabled, y: SharedReadWrite]. This keeps the two (singleton) blocks of SharedReadWrite apart, so even after reading from x, a subsequent write to x will still invalidate y.

Conclusion

That’s it already. You can find a complete description (but without explanation) of Stacked Borrows 2.1 in the UCG repository.

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

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

Posted on Ralf's Ramblings on May 21, 2019.
Comments? Drop me a mail or leave a note in the forum!