Permissive Borrows

language design Unsafe Code Guidelines
1

cc @RalfJung, who asked me to write up my thoughts on a new aliasing model

I've spent a lot of time recently working on a new aliasing model, which I call Permissive Borrows. This post is meant to introduce the model. It's written vaguely in the style of an RFC, as I consider it to be a good style for conveying new ideas, but isn't a proper RFC or pre-RFC because it isn't suggesting any particular course of action (in particular, it does not discuss alternatives or prior art, things that should definitely be considered before making any decisions), so it just abruptly ends after explaining the idea and a couple of variations on it.

It is quite possible that this document contains mistakes, either due to things that I haven't considered, or due to a failure to correctly translate my thoughts into writing. It's also probable that I haven't picked the best way in which to explain my ideas, and it may be that a different way of stating things would be clearer.

Motivation

Rust's existing aliasing models, Stacked Borrows and Tree Borrows, effectively separate pointers and references into two groups: references &'a T / &'a mut T that borrow the memory they target for the entire lifetime 'a (which starts and ends in the same stack frame), and everything else. For references in the first group, they provide a good level of optimization. But for references in the second group, they do not provide much optimization help: such references allow operations that would be undefined behavior in Stacked/Tree Borrows if they were performed on shared or mutable references, and thus need to be given exceptions or opt-outs (which typically leave code that uses such references almost unoptimized).

Rust has a lot of types of references that don't quite fit into the first group, but nonetheless have aliasing guarantees that should in theory allow for a high level of optimization. In particular, many types of reference act like &T or &mut T but do not have a known lifetime, or have a lifetime that does not necessarily start and end in the same stack frame:

  • Box<T> (lifetime ends when dropped, not at a specific point in time);

  • Borrow types of RefCell (lifetime can be ended early by dropping it, potentially in a different stack from from where it started);

  • Anything that gets borrowed across an await point inside an async future or other coroutine (you can poll the coroutine in one function, then when it halts at an await, call another function that polls the coroutine, causing the borrowed value's lifetime to end in a different stack frame from where it started).

At present, these situations are handled either by not optimizing them (e.g. the current compiler does not make use of aliasing assumptions between the local variables of an async block), or using hacks to allow the compiler to pretend a type is in the first group after all (e.g. Box is optimized by pretending that an old and new allocation point to different memory even if they have the same address, but this model only works if memory allocations come from entirely outside the Rust virtual machine, so it is incompatible with inlining the allocator and is incompatible with custom allocators written in Rust).

Additionally, a coroutine can borrow from itself, without invalidating an outside reference to the coroutine as a whole (meaning that a coroutine's local variable can be simultaneously borrowed by two unrelated references), and this situation was not envisaged by Stacked Borrows or Tree Borrows and thus needs a special case to deal with it. The currently planned solution is to use UnsafePinned as the special case, but this has the side effect of removing almost all ability to optimize futures (because UnsafePinned is permissive enough that the compiler can no longer prove that the future is not stored inside its own local variables, meaning that it has to be reloaded from memory whenever the vairables are written).

Permissive Borrows is designed as an aliasing model that is capable of optimizing situations like this: it does not assume that lifetimes start and end in the same stack frame (except for types that are impossible to move or drop and thus necessarily survive throughout an entire function), and is even capable of justifying many optimizations on self-referential coroutines.

Guide-level explanation

Permissive Borrows is an aliasing model: set of rules that allow the compiler to assume that a program will not access memory in certain ways, so that it can optimize code based on that assumption. Aliasing models work by defining certain operations to be undefined behavior, so that optimizations that would be broken by those operations are valid (on the basis that if those operations do not occur, the optimization is valid, and if they do, the code has undefined behavior and so any optimization is valid).

In Permissive Borrows, the main requirement is that if you do something that contradicts the aliasing requirements of a reference, you do not use that reference again:

  • If you write to memory that was used by a shared reference (except inside UnsafeCell), you must not use that shared reference again (because the write indicates that the shared reference's lifetime has ended);

  • If you access memory that was used by an exclusive reference (except inside UnsafePinned), using a reference that is not based on (e.g. reborrowed from) that exclusive reference, you must not use that exclusive reference again (because the conflicting access indicates that the exclusive reference's lifetime has ended);

  • If you access memory through an exclusive reference, you must not use any reference or pointer based on that exclusive reference again. (This is because using an exclusive reference ends any reborrow of that exclusive reference.)

Permissive Borrows considers Box and &own to be types of exclusive reference in addition to &mut.

What counts as a "use" of a reference depends on the exact type of the reference. References that are expected to point to valid memory (such as &T and Box<T>) are considered to use that memory from when they are created to when their lifetime ends. For types like &T and &mut T that cannot be moved or dropped and are provided as a function/method argument, they are considered to still be in use when the function ends, as there is no way to drop them early. For types like Box<T> which can be dropped, their lifetime is considered to end at their last use, because they might be dropped early to repurpose the memory.

Some references are not necessarily expected to point to valid memory: for types like MaybeDangling<&mut T> which might not be valid, the rules are only enforced for references that are actually accessed through. For references to coroutines (that might be borrowing values from themselves), the reference is only considered to use any given memory address between its first and last access to that address (before the first access, the address might potentially have been borrowed by the coroutine, but an access directly through the reference proves that any such borrow has ended).

Reference-level explanation

(In this explanation, "provenance" refers specifically to the component of provenance used to track aliasing violations. This is not meant to preclude the possibilty that other types of provenance exist.)

As with most aliasing systems, Permissive Borrows tracks pointers and references using their provenance. Permissive Borrows assigns a new provenance to the result of almost any attempt to derive one pointer/reference from another (via reborrowing, reference-to-pointer conversion, or borrowing a dereference of a pointer); the exceptions are reborrowing a shared reference as another shared reference, and operations that convert a raw pointer directly (or via a place) into another raw pointer, which retain the same provenance. Each provenance has a parent (which is the provenance that it was created from), making it possible to determine a provenance's ancestors and descendants.

For the purpose of Permissive Borrows, reference/pointer-like types that assert ownership (e.g. &own and Box) are considered to be types of exclusive references, but different types from &mut; "exclusive reference" refers to these types collectively, but &mut only to mutable types in particular.

For each provenance, define that provenance's range as the set of memory addresses that have ever been accessed through that provenance and its descendants. The basic idea of Permissive Borrows is to consider a pointer/reference R to be valid at a particular type T if, since a specific time (specified below), nothing has happened that would disable the ability of a pointer/reference with that type and provenance to access any memory address in the provenance's range. However, a provenance also becomes invalid when any of its ancestors are used as an exclusive reference, and a pointer/reference with an invalid provenance (or no provenance at all) is considered invalid at every type.

The events that disable accesses are as follows:

  • Any write to a memory address disables the ability of shared references to access that address, unless the type of the shared reference considers the address to be inside UnsafeCell;

  • Any memory access through a pointer/access P disables the ability of exclusive references to access the same address, unless the exclusive reference has the same provenance as P or a provenance that is an ancestor of P's, or the type of the exclusive reference considers the address to be inside UnsafePinned.

Depending on the type T of a reference R, there are two possible time periods that might be checked for disabling accesses that might invalidate R at type T:

  1. If T has a target that is a coroutine that borrows or reborrows from itself, R is only disabled by a disabling access to an address A if R's provenance first accessed A prior to the time at which the disabling access occurred.

  2. In other cases, R is disabled by a disabling access to an address A if the disabling access happened since R's provenance was created.

It is undefined behavior to:

  1. Perform a memory access through a reference/pointer R at type T, unless R would be valid at type T immediately after the access (this implies that R must also be valid at type T immediately before the access);

  2. Typed-move, typed-copy or reborrow a reference/pointer R at type T, unless either R is valid at type T and all memory it could access (based on its address and type) can be accessed without faulting, or R is contained in a wrapper like MaybeDangling or MaybeUninit that is intended to allow the storage of invalid references;

  3. For references R that are function/method arguments whose type inherently prevents them being moved or dropped (&T or &mut T, either directly as the type of the argument or as a field of a Copy struct or Copy enum), do anything during the execution of that function/method (and functions/methods it calls into) that would make a reborrow of R at that type undefined behaviour under rule 4.

For example, suppose a &T (where T has no special aliasing properties) is reborrowed from a &mut T, with the &T used to read the value at an address, then the &mut T is later used to read the value at the same address. Based on rule 2, the &mut T is valid as long as all accesses to that address since it was created have been through that reference and its descendants. Although the address was added to the range of the &mut T due to a read through a &T, the type of the original read does not matter when determining whether the &mut T is valid (e.g. it would be possible to write to the address through the &mut T between the two reads, and the reference would still be valid).

The rules above are not quite enough to allow the desired optimizations due to the possibility that weird aliasing situations could be created via transmutes or untyped copies. There is an additional rule to rule out these situations:

  1. Whenever an access is made via an exclusive reference, anything else with the same provenance as that exclusive reference loses its provenance (i.e. its provenance is removed, or set to a null provenance).

Optimizations this permits

Rules 1, 3 and 6 are sufficient on their own to permit two main types of optimizations:

  • As long as they stay in the same relative order, reads or writes through a reference and its descendants (other than inside UnsafeCell/UnsafePinned) can be moved to later points in the code, as long as they do not move beyond the last read or write through that reference that can be guaranteed to happen and reads and writes through the same reference;

  • As long as they stay in the same relative order, reads or writes through a reference and its descendants (other than inside UnsafeCell/UnsafePinned) can be moved to earlier points in the code, as long as they do not move before the first read or write through that reference to the same address.

These two basic optimizations can be used as components to build up larger optimizations. The most notable are autovectorization (which can be done by postponing writes to perform them in batches, causing the reads to also be performable in batches because any writes between them were moved out of the way), and loop-invariant code motion (which can be done via moving all the reads of a single address back to the point of the first read of that address). I consider these to be the most important optimizations (because they give much larger savings than most and can be difficult to replicate by rearranging the code by hand), and it is a big advantage of Permissive Borrows that they are possible even in the case of a coroutine that borrows from itself.

Most references are not to coroutines that borrow or reborrow from themselves, so can use rules 2, 3 and 6 instead. This gives a little more optimization power:

  • As long as reads or writes through a reference and its descendants (other than inside UnsafeCell/UnsafePinned) can be proven to happen, and as long as they stay in the same relative order, they can be moved to any point in the code between the point at which the reference was created and the last read or write through that reference that can be guaranteed to happen.

The main optimization advantage gained here is the ability to optimize a memmove into a memcpy: in memmove situations (like reading a large array from one reference and writing it into another), the rule 1+3 optimizations do not help because all the reads are bunched together already, and likewise all the writes are bunched together, so they cannot be moved to interleave them; whereas the rule 2+3 optimizations allow moving some of the writes earlier in order to interleave the reads and writes.

The optimization gains from rules 4 and 5 are much smaller, primarily allowing speculative reads in cases where the program's control flow might not guarantee that the read happens, or postponing reads beyond functions that might potentially free or reuse memory. (Rules 2+3+4 justify LLVM's dereferenceable; 2+3+4+5 justify dereferenceable, noalias and nofree (and readonly for shared references). But most of the optimisations noalias permits are already permitted by rules 1+3 or 2+3, just for a different reason, so the gain from noalias is small.)

Permissive Borrows is expected to give a much larger scope for optimization than Stacked/Tree Borrows do. This is because Stacked Borrows and Tree Borrows are unable to soundly optimize certain types (e.g. Box with a custom or inlined allocator, &own, borrows from RefCell, closures that reborrow from themselves), and thus compile these types with no optimization (in particular, LLVM's noalias is not valid for these types); but most of the optimizations allowed by Permissive Borrows still work even on types like these (meaning that they can be heavily optimized even in the absence of noalias).

Variations

Blocking the reborrow of a mutable reference from a shared reference

As written, Permissive Borrows makes it possible to reborrow a mutable reference from a shared reference, as long as the shared reference is never used again (and is not a function/method argument). This seems to naturally fall out of the definitions (and some similar operations are intentionally allowed, e.g. you can convert an exclusive reference to a raw pointer, then mix that raw pointer freely with raw pointers that were not based on the exclusive reference, as long as you never use the exclusive reference again; and doing so is useful and intended because many implementations of deallocation work like this). It also provides a simple way to implement two-phase borrows (reborrow as shared, then upgrade by reborrowing the shared reference as mutable).

Oddly, blocking the ability to reborrow a mutable reference from a shared reference does not seem to allow any additional optimizations. On the other hand, being able to do that is extremely weird and counterintuitive for most Rust programmers, so it might make sense to ban it regardless. There seems to be no benefit to making it undefined behavior (other than allowing Miri to shout at people who try it); perhaps it could/should be considered erroneous rather than undefined behavior.

(EDIT: I found a reason to make this undefined behavior: it allows the caller of a function to prove that the callee does not change a piece of memory on the basis that it hasn't been given any references that are capable of writing to it, in cases where it moves a shared reference into the function it's calling (via a wrapper) rather than reborrowing it. This situation is a little hard to formalize (due to the possibility of reborrows via raw pointers) and probably fairly rare, but a rule to cover it might nonetheless be useful.)

Changing the rules for when rule 5 applies

Rule 5 is the equivalent of a Shared Borrows "protector" (i.e. a special case that requires a reference that's a function argument to be alive and valid for the whole function).

In Stacked Borrows, protectors are used to justify LLVM's "noalias" attribute. Right now, there aren't many easy ways to communicate aliasing information to LLVM, so being able to apply "noalias" to a function parameter is important in the short term (to avoid a situation in which the aliasing model is able to justify a lot of optimizations but the compiler is unable to communicate this fact to LLVM).

There are two possible ways to vary this. One possibility is to make rule 5 apply to more types, e.g. also applying it to references that can be dropped. My experience is that putting protectors on such types is extremely unintuitive: I consider it to be natural to assume "I have dropped this reference and thus I can reuse the memory it pointed to without causing aliasing variations". I have in the past accidentally written code that is unsound under Stacked and Tree Borrows due to making this assumption, and I'm not the only such person (such code existed in the Rust standard library for many years, and could theoretically have caused miscompiles). I'm assuming that in the long term, we will find a way to allow LLVM to optimize such references even in the absence of noalias (especially as Permissive Borrows gives precise rules for how you would do so), in which case noalias would give only a very small gain.

Another alternative is to (once LLVM is able to optimize on the basis of rules 1/2/3: it can already translate rule 4) remove rule 5 altogether, on the basis that the gain is fairly marginal compared to that of the other rules, and it adds a significant amount of complexity. There are a few optimizations that would be lost in theory, and LLVM does attempt these on occasion. In my experience, these optimizations are not very successful in practice with current LLVM: they are often missed in cases when they would help, applied in cases where they don't help, or disabled for performance reasons. As such, after implementing the other rules, there may be a case for removing this one (or perhaps locking it to a high optimization level). That said, there is potential that rule 5 could become more useful in future.

9 Likes
2

Interesting. This would benefit greatly from some examples comparing your model with Tree Borrows:

  • Code snippets that would be UB under one model but not the other
  • Optimizations (as shown with before-and-after code snippets) that are valid under one model but not the other

This is especially valuable for cases where you have less UB than Tree Borrows. Previous attempts to do this have often ended up either being unsound or not allowing desirable optimizations.

I realize your proposal already discusses this to some extent, but it should be fleshed out so it’s easier to understand (and easier to try to poke holes in :slight_smile:).

2 Likes
3

As a starting attempt to poke holes:

  • The way rule 6 is worded is suspicious. Normally provenance is supposed to work as similarly as possible to normal data. For example, an immutably borrowed pointer cannot change its provenance any more than it can change its address. But rule 6 would violate that. This might hinder other optimizations in unexpected ways – or it might not. But if it doesn’t, then that’s probably because there exists some equivalent formulation of the rules that avoids provenance zapping. Perhaps copies could automatically create some kind of modified provenance (not necessarily the same as a normal derived provenance).

  • Borrowing shared into mutable will not work if the shared reference points to read-only memory, such as global variables in .rodata, memory mappings performed as read-only, etc. So if you want to allow borrowing shared into mutable in other cases, you’ll need to treat this as a separate restriction – which is possible, but does add some complexity.

2 Likes
4

I was hoping to add a more extensive list of what optimizations were/weren't allowed as part of the initial post, but after spending over a week trying to figure out what to write, then several days to build up enough courage to write it, I decided to post what I'd come up with so far rather than delaying for weeks trying to make the original presentation perfect.

There are three ways in which changing the aliasing model can change the amount of UB: it can remove UB; it can directly add UB; or it can indirectly add UB as a consequence of removing UB (because in an aliasing model which has a lot of UB, a lot of standard library code can't be written using references and has to use raw pointers instead; but when you change to an aliasing model which has less UB, the standard library can be written using references rather than pointers, and that can increase the UB/optimization opportunities for uses of the library).

It may take me a while to write about the removed UB (and UB that becomes added as a consequence), but the two hole-poking attempts in the above post are both closely related to the added UB, so it makes sense to discuss the added UB and the holes together. The only directly added UB that I'm aware of is related to situations where two references/pointers have the same provenance, but accesses through one should conflict with accesses through the others (this situation normally implies that a reference has been transmuted or a non-Copy reference has been untyped-copied). This situation is known to be somewhat problematic in Stacked Borrows and Tree Borrows, and is discussed in this unsafe-code-guidelines issue. It also causes some problems for Permissive Borrows in the absence of an explicit fix for it (there are fewer problems but they have a more significant effect).

Consider code like the following (playground). and its variations where the nested references inside foo's argument a are changed to other types among &usize, &mut usize, &Cell<usize>:

#[inline(never)]
pub fn foo(a: &mut (&usize, &mut usize)) -> usize {
    let x = *(a.0);
    assert!(x == 1);
    *(a.1) = 2;
    *(a.0)
}

pub fn main() {
    static mut X: usize = 1;
    let mut a = (&raw const X, &raw const X);
    let b: &mut (*const usize, *const usize) = &mut a;
    let c: &mut (&'static usize, &'static mut usize) =
        unsafe { core::mem::transmute(b) };
    let d = foo(c);
    dbg!(d);
    dbg!(unsafe { X });
}

The code contains two functions, foo which is safe Rust, and main which contains an extremely dubious transmute (giving foo an argument where the two inner references alias each other). However, all the variations where a.1 is writeable (either &Cell<usize> or &mut usize) are accepted by Stacked Borrows and Tree Borrows (which consider them to not be UB). A consequence of this is that the second read of a.0 cannot be optimized out in foo: because the aliasing model allows a.1 and a.0 to alias each other, the optimizer cannot assume that a.0 is still 1 at the end of the function, even though it was asserted to equal 1 earlier in the function.

This program demonstrates a few different things. One of them is that it may not be the aliasing model's job to prevent writes into read-only memory: in this configuration of this program (with the &usize and &mut usize), the program writes into memory backed by a &usize while the &usize is live, and then reads the value afterwards. You can replace the static mut in the first line of main with static, and then the program does have undefined behavior, but it is still fine from the aliasing model point of view (the undefined behavior is caused by a separate unrelated rule that disallows writing into memory that was allocated by a non-mut static, and Miri won't specify that the violation is due to Stacked Borrows or Tree Borrows rules, like it does for aliasing violations). Although it would in a sense be nice if the aliasing model were accurate with respect to preventing writes into read-only memory, the existing aliasing models don't do that and it is probably best treated as a separate concern.

It also demonstrates the added UB from Permissive Borrows, which (if I haven't made a mistake) is all in programs like this (although not always for the same reason). There are two reasons why I think it's desirable for programs like this to be considered UB (unless both the inner references inside a are &Cell<usize> in which case it is of course fine):

  1. It makes optimizations easy to implement, by providing a rule that's both useful for optimizers and easy to understand. Permissive Borrows is intended to justify optimizations that assume that if you access the target of a shared reference twice, it still has the same value, and if you access the target of an exclusive reference twice, any changes in between will have been made via pointers/references derived from that exclusive reference. This is basically the same rule as LLVM noalias, except that the timing is different (instead of covering the entire body of a function, it spans from the first use of the reference to the last), so it justifies the same optimizations but in a different scope. (This rule is implemented by rules 1, 3, and in some cases 6; rules 2 and 5 are special cases that increase the scope in which the reference is considered unaliased, thus allowing further optimization, but they aren't really the core of the aliasing model.) If code like main above is not considered UB, then these optimizations don't work, which makes the aliasing model less powerful and harder to implement.

  2. Code like foo (the safe function) is extremely common, so it would be nice to be able to make aliasing assumptions about it in order to be able to optimize it. In particular, "this function's argument is a reference to a struct/enum whose fields are treated like local variables" is the current desugaring of coroutines (which in turn are the current desugaring of async). Pin (as opposed to Unpin) isn't visible to the aliasing model, so foo above could easily be part of the desugaring of the Future implementation of the closure generated by an async block or function that looks something like this:

    let a0: &usize;
let a1: &mut usize;
/* ... more code, including an await ... */
let x = *a0;
assert!(x == 1);
*a1 = 2;
do_something_with(*a0);

    One of my goals with Permissive Borrows is to make async blocks capable of aliasing-related optimizations. Cases like the example in this post mean that Stacked Borrows and Tree Borrows do not have enough UB to do even basic aliasing-related optimizations on the local variables of an async block (this "an immutable reference keeps its value" optimization assumption is the assumption required for loop-invariant code motion, one of the simplest and highest-value optimizations, so it would be a shame if the aliasing model didn't justify the assumption).

In the specific version of foo written above, where the target of a &usize is changed via a &mut usize, Permissive Borrows considers calling it with the inner references aliased to be UB even without using rule 6. Specifically, the read from a.0 is allowed, and so is the write to a.1, but doing so disables a.0 in the case where a.0 and a.1 alias, meaning that the subsequent read back through a.0 becomes undefined behavior (based on rules 1 and 3 or 2 and 3). The same thing happens in all cases where either a.0 or a.1 is a (non-interior-mutable) shared reference (writing directly through such a shared reference would be immediate UB, although the compiler typically refuses to compile such code anyway; and writing indirectly to a non-interior-mutable shared reference's target, either through a reborrow of the shared reference or via an unrelated pointer/reference, makes any further uses of the shared reference UB).

The problematic cases are when a.0 and a.1 are either both exclusive references with the same target and provenance, or when a.0 is an exclusive reference &mut usize and a.1 is an interior-mutable &Cell<usize> with the same target and provenance. These cases are a very long way away from the sort of code most Rust programmers expect to work, so it's reasonable to make them undefined behavior, and they also cause considerable problems for optimizers (which want to be able to assume that any value they read or write through an exclusive reference will stay there). Rule 6 was added specifically to address these cases.

I agree that the "let's zap all copies of this provenance elsewhere in memory" rule is unusual. In fact, through most of the time I was working on this aliasing model, I was using a more normal pair of rules in its place, which I'll call 7 and 8 for ease of reference:

  1. When performing a write through a mutable reference, its provenance is replaced with a fresh provenance (with all aliasing-related tracking other than the contents of memory updated to use the new fresh provenance), and any future accesses through its old provenance are considered undefined behavior.
  2. It is undefined behavior to access the same memory through the same provenance but as two different types, if one of those types considers the memory to be the target of an exclusive reference (i.e. &mut without UnsafePinned), but the other doesn't.

Rules 7 and 8 are compatible with the "provenance is just like you're coloring the bits in memory" model that I think Rust is generally using at the moment, and don't require a remote provenance zap. However, when I discovered rule 6, I realized it was just generally better:

  • The UB added by rule 8 is a bit surprising (and somewhat reminiscent of C's type-based aliasing analysis that Rust has rejected), so there's a chance that people could run into it by mistake (e.g. by transmuting a reference rather than reborrowing it), whereas it's only really useful to save the optimizer from having to worry about one specific code pattern that almost nobody would ever intentionally write;
  • Rule 7 makes it UB to subsequently use the outer reference of an & &mut T if the inner reference is used to perform a write (and although & &mut T acts basically like a shared reference in current Rust, this is still more UB than many people might expect);
  • Provenance zaps might be a little complicated from an opsem point of view, but are very easy for optimizers to work with, because removing provenance from memory makes some operations that would otherwise be legal into UB and otherwise has no effect (so the optimizer need only worry about them in the specific cases that they want to make use of them). When you're implementing an optimizer, rule 6 basically just becomes "if you access memory through an exclusive reference, you know that any access through an aliasing reference (within the appropriate scope) would be undefined behavior, so you can assume that no such accesses are happening and optimize accordingly", which is the exact rule that most optimizers care about.

The aliasing model would work fine with rules 7 and 8, but it would have a little UB, and be a little more complicated, for no real benefit other than having provenance be treated strictly as a sort of metadata that you glue onto the bits of a pointer, and I'm not convinced that that's the right model for provenance anyway. (In particular, it seems both well-defined and useful to be able to transmit provenance through things that are smaller than pointers, to the extent that some libraries I've worked on have had the need for ZSTs with provenance; but if you're storing provenances only on the bits of a pointer, there's no way to store it in a ZST. My current workaround is to store it on the exposed provenance list, but this has its own issues, such as not correctly working in LLVM at the moment.)

The changes to ban &mut aliasing other references with the same provenance are intended to be the only directly added UB in Permissive Borrows, but there's one other case which might (depending on other opsem decisions) have more UB than Stacked Borrows and Tree Borrows: what happens if you use a pointer derived from a reference to access memory outside the memory the reference points to. Currently, it is undecided whether or not doing that is legal: it might be decided to be unconditionally undefined behavior to do that (a "subobject provenance" model), in which case the choices made by the aliasing model have no effect on it. However, Permissive Borrows does have some opinions about what would be considered undefined if there were not a subobject provenance rule (e.g. if one &mut accesses a byte of memory, then an unrelated &mut accesses the same byte of memory, the original &mut is not usable to access anything anywhere in memory, even if the byte in question was not within the target of either &mut). I'm not entirely sure on how Stacked Borrows and Tree Borrows treat this case, but think it's possible that their decisions may be different from those made by Permissive Borrows.

I do intend to write about the UB that is removed by Permissive Borrows (and the UB that might be added back as a consequence of the standard library using references more heavily, and raw pointers and aliasing-rule-suppressing wrappers less heavily, as a consequence), but it may take me some time to get my thoughts on that together and to actually write a post about it, so I thought I'd post this post now even though it isn't enough on its own.

5

I'm worried about the pointer zapping. Is there anything in Rust right now that violates uninit refinement? Replacing uninit bytes with the wrong init-bytes-with-provenance would introduce UB with this pointer zapping.

Second, less significant, the concrete example with two aliasing mutable references may be absurd, but I'm not immediately certain that there's no plausible highly-generic code + plausible use case that:

  • creates two copies of a pointer with identical provenance,
  • does not read/write through one of the copies, but still keeps it around, and expects that copy to be immutable,
  • writes through the other pointer, as a &mut T. (This requires there be no retag when, say, reading that other pointer from wherever it's stored in memory.)

I think some oneshot::{Sender, Receiver}-like patterns can satisfy the first two conditions, but after trying to find a plausible example that's UB in your model, I feel comfortable saying that the third condition seems extremely unlikely to be doable unintentionally.

6

I don't think this violates uninit refinement. If you replace uninit bytes with the wrong init-bytes-with-provenance and they get zapped, you end up with init-bytes-without-provenance (rather than UB), and can still use them like normal initialized bytes. You only get UB if you try to dereference through them (but doing so is indistinguishable from trying to dereference in violation of the aliasing model). Or to put it another way, a provenance zap is actually unobservable, as anything that would have tried to make use of the provenance could be considered UB due to violating the aliasing model.

As for the second problem, Permissive Borrows intentionally creates a new provenance whenever you convert a raw pointer into an &mut by normal means, in order to try to keep unique references uniquely identifiable. In order to create an &mut with identical provenance to the raw pointer (rather than a new provenance that derives from it, which wouldn't cause problems), you need to do something like cast a pointer to it from *mut *mut T to *mut &mut T and then dereference the result (and even that doesn't cause problems unless you then try to dereference the original raw pointer that has the same provenance as your weirdly transmuted reference).

7

But in the Abstract Machine, the zap performs a write, correct? Which could cause UB if the zapped pointer was required to be immutable, or if it'd cause a data race.

....ah. but the only thing which cares about those writes would be the aliasing model.

So your model could require that, say, memory behind a &-without-UnsafeCell is immutable except for provenance zaps, that data races are prohibited except for provenance zaps, and so on.

8

This is written in an extremely confusing style, since most people would agree that Rust only has those two reference types. You are using "reference" in a different sense here to include user-defined smart pointers, without saying that, leaving the reader very puzzled for a while.

This is wrong. We are not pretending anything. Address reuse is entirely fine. Aliasing is not about address identity, it is about whether accesses can be reordered.

So, I think you have to remove Box from your list. We support the aliasing restrictions of Box just fine.

FWIW these would be trivial to support in TB if we added a way to suppress protectors while maintaining the rest of the aliasing rules and effects.

So, permissive borrows has more UB than SB/TB and is therefore less permissive? :wink:

So you actually want to mutate the memory that stores these other provenances? That's a terrible idea IMO. What if they are stored in read-only memory? What if they are stored behind an &T, which you just invalidated? How is one supposed to do local reasoning if the language has an operation that may mutate stuff all across the program's memory?

Everything I know about reasoning about programs tells me that we should not do this. If you can, I would suggest instead having those pointers keep their provenance, but making it so that the provenance is now "disabled" and can't be used for accesses again, similar to TB. If that doesn't work then I think your entire model doesn't work.

Also up to this point I still have not found a significant difference to Tree Borrows, apart from this odd global provenance adjustment rule, so I am unsure which problem in TB this model is attempting to fix. I guess I'll have to re-read every word in detail, but it'll be quite a while until I have that kind of time. The document would be much easier to read if it highlighted such high-level points rather than leaving it up to the reader to extract the relevant gems from a haystack of information.

And it seems the rules of the model end here, the rest of the post describes consequences/variants of these rules.

Box with an inlined allocator is entirely fine with SB/TB. And Box with a custom allocator is fine too, we just need to add the NativeAllocator wrapper that has been mentioned in discussions multiple times.

NativeAllocator will require StaticAllocator, so one case where TB has problems is Box with a bump allocator, as those are not StaticAllocator. However, that problem is mostly caused by LLVM allowing very strong optimizations around native allocators, which are incompatible with bump allocators. If LLVM ever gains weaker notions of native allocators, I don't foresee issues with also exposing them on Rust and having noalias on such Boxes.

The same is true in Tree Borrows (without the implicit-write options).

I think that's fine; in Miri, this is already a separate flag. In TB, if you take an &raw const to a static S: i32, and then cast the raw pointer and write to it, the aliasing model has no objections to that, only the "read-only allocation" check complains. This causes trouble for statics that are partially interior mutable, which is kind of annoying: CTFE cannot access any field of a static if a single one of them has interior mutability. · Issue #156789 · rust-lang/rust · GitHub.

9

I disagree: aliasing models designed along the lines of Stacked Borrows and Tree Borrows are unable to place aliasing requirements on boxes without assuming that they allocate fresh memory each time. In fact, Miri currently flags UB whenever an allocator reuses memory that was allocated upon entry to the current function (but has been deallocated during the function). I just filed a bug about this (The protectors on custom allocators can violate Stacked Borrows and Tree Borrows for otherwise sound code · Issue #5284 · rust-lang/miri · GitHub), because I was very surprised that this was not already a known limitation.

This is exactly the same problem that previously occurred with RefCell. I thought this was a widely known limitation of Stacked Borrows and Tree Borrows (in particular, the fact that they do not have much optimization power for allocations made with custom allocators because they cannot soundly place protectors on them), and one of my main motivations behind the design of Permissive Borrows was to create an aliasing model that is capable of optimizing them (because custom allocators aren't very useful if the compiler doesn't make aliasing assumptions about them, and IIRC the only aliasing assumption that the compiler actually makes at present is noalias which is only justifiable in the presence of protectors).

10

This sounds exactly like TB, except that the UnsafePinned part is not implemented in TB yet, and this model does not account for the complications needed to actually support two-phase borrows -- but if this model was fixed to survive contact with reality I think it'd end up with the same two-phase handling as TB.

As written I think this model declares the typical v.push(v.len()) as UB because the mutable reference passed to push gets invalidate by the read in len.

This is the major divergence from TB, right?

:thinking: I am very "opsem coded", I have a hard time figuring out what the consequences of this are. It certainly sounds like a bunch of state needs to be tracked to figure out which events happened in which order.

There are many notions of "validity" and it is unclear which one you mean here. Is this different from TB's rules?

We have formal proofs of correctness of optimizations for SB/TB in a model that allows reusing the basic identifiers of allocations that serve as locations. So, you are just wrong.

Memory has to be fresh as in "not currently allocated" of course, but the same memory (as in, absolute address, or in our formal model "allocation ID and offset") having been previously allocated and then freed is entirely fine.

Maybe you mean something else by "fresh", but with the usual definition I would use, SB/TB are fine here.

11

I don't think that works. Optimizations based on no-data-race and no-write-behind-& work on the Abstract Machine level, so they need the full AM-observable data in memory to stay the same, including provenance.

I will consider such global-provenance-zap models to be infeasible until someone actually proves data-race-UB-based optimizations correct in such a model. I have very strong doubts that this is possible since everywhere that you previously proved "I will get the same value" you now prove "I will get a value with potentially different provenance" and that may introduce UB into previously UB-free programs.

12

I realised a while back that all Rust aliasing models are likely to look very similar to each other, simply because they have to match the semantics of Rust and that adds a lot of constraints.

I think one very big difference from SB/TB is that it doesn't rely on retags to operate correctly. In TB, retagging increases the amount of undefined behavior, whereas the closest PB equivalent, the "generate a new provenance upon a reborrow or a reference/pointer conversion", reduces it. (In particular, TB does not generate a new provenance when a reference is converted to a pointer, whereas PB has to.)

I looked at that repository. Exactly one of the optimizations proved there appears to work on boxes with custom allocators (that if you retag a mutable reference and then write to it, a subsequent read will still read the same value – presumably boxes would be optimized as though they were mutable references). The rest don't work on boxes with custom allocators, either because they require a protector (which would be unsound), or because they are only correct on shared references.

This has made me realise that we are thinking about optimizations in a fundamentally different way from each other, though (which may make discussion difficult). I've been thinking about correctness of optimizations at the asm level (e,g, the UB provided by the model gives the compiler the freedom it needs to generate assembly code that performs certain operations in a different order from that specified by the program, but this is considered to not be a change to the program as seen by the Rust abstract machine, just a particular method of implementing the Rust abstract machine). Instead, the Tree Borrows paper seems to be thinking more along the lines of "you can apply a specific program transformation on a Rust program to produce a different Rust program, but it has the same semantics", which is more restrictive (because the resulting program has to have the same aliasing model effect rather than just the same runtime behavior). I'm not sure whether this is a significant difference, but it might be.

13

Yeah to be clear that's entirely fine. :slight_smile: I would hope that this makes it easier to compare models as they are all kind of similar, but unfortunately that's not so easy with your writeup.

Interesting, that is a big difference indeed. I am not sure how that's supposed to be possible. Your model talks about parent references. Without retags, I don't think that's a well-defined notion. Without retagging, provenance doesn't change, and if provenance doesn't change, there's no sense in which one pointer is the "parent" of the other.

Note that if we get around to implementing Refresh provenance of global allocator · Issue #2686 · rust-lang/miri · GitHub, and if you port your example to be a global allocator, SB/TB will work just fine with that without any further changes.

Boxes with custom allocators via NativeAllocator (or with a user-defined global allocator) get protectors of course. Like all boxes they get "weak" protectors, which I am not sure we covered in our proofs, but I see no reason that the proofs would not generalize to weak protectors.

The repo uses the standard definition of "correctness of an optimization" (contextual refinement). That's not really up for debate.

The one thing that is up for debate is the language you do the optimizations on. For this repo we are assuming that the IR used for optimizations also has SB/TB as its memory model, which is not required. But if it uses a different memory model then you still have to describe that model and argue for correctness of the optimizations so that doesn't really change anything about what you need to do to convince us. You now have to define two models, one on Rust and one on the IR. :wink:

Using any thinking on the asm level for optimizations is just wrong. Optimizations occur on the IR, not on asm. Other optimizations want to run after your optimizations, so you need to argue that the optimization is a valid transform in the IR that the following optimizations are also expressed on. Eventually, the IR gets lowered to asm, and you need to argue why that is correct for your model, but that is usually trivial since all the "ghost" state (provenance) gets erased here. And then when you are at the asm level you cannot do provenance-based optimizations any more obviously.

14

Pretty much. I don’t love the idea either, I’m just more willing to grant it as “probably feasible but very time-consuming to implement”. I should read more about the optimizations we apply to better tune my intuition.

15

I was assuming that there would indeed be multiple languages involved, and am using the standard definition of an optimization refinement. However, I assumed that optimizations would work as follows: certain operations are undefined behavior on the Rust abstract machine; so the compiler can refine a Rust program by adding assertions about its behavior (which might not necessarily be expressible in Rust itself, but can be expressed in terms of the abstract machine), on the basis that any program where those assertions weren't true would have undefined behavior; and then those assertions get lowered into a different language (maybe MIR or LLVM IR) along with the program, and those lowered assertions are then used to justify optimizations in the lower-level language. LLVM noalias and dereferenceable are good examples of this sort of assertion.

16

I am not sure why you are now restricting yourself to custom allocators. Your earlier claim was that SB/TB would not work with allocators that reuse addresses. The global allocator in Rust does not guarantee fresh addresses. Miri will even reuse addresses under some conditions. So if your claim was correct, TB would not work with the normal global allocator. But your claim isn't correct, and it is unpleasant to be in this conversation where you are repeatedly making incorrect claims in very definite tone, even after being called out for your prior incorrect claims. I will bail out soon.

I was assuming that there would indeed be multiple languages involved, and am using the standard definition of an optimization refinement. However, I assumed that optimizations would work as follows: certain operations are undefined behavior on the Rust abstract machine; so the compiler can refine a Rust program by adding assertions about its behavior (which might not necessarily be expressible in Rust itself, but can be expressed in terms of the abstract machine), on the basis that any program where those assertions weren't true would have undefined behavior; and then those assertions get lowered into a different language (maybe MIR or LLVM IR) along with the program, and those lowered assertions are then used to justify optimizations in the lower-level language. LLVM noalias and dereferenceable are good examples of this sort of assertion.

LLVM noalias needs to have its own model of course. So unless you are describing that other language and its assertions in detail I will have to assume that it uses the memory model you describe, not some other unspecified model that you claim exists and that you claim can do certain optimizations, without showing that model. The model that does the optimizations is the interesting one, if that's different from your writeup and from every prior model then it is impossible to evaluate your proposal.

17

I didn't think there was / didn't draw a distinction between "custom allocators" and "allocators that reuse addresses" (in the sense of "same address and same allocation ID"). It is hard to hold a conversation at high speed while also keeping to a high level of precision.

Trying to be precise: one of my main motivations for creating a new aliasing model is that in SB/TB, if a Box has a protector applied to it and is deallocated during the period in which it is protected, any attempt to create new Boxes during that time period, within the same memory, must treat the new memory as being different from the old memory (in a way that means it does not violate the protector). Such protectors are incompatible with Box implementations that for whatever reason need the memory to be considered the same. I believe both that such Box implementations are valuable (and likely to occur in practice), and that a higher level of optimization on such Boxes than SB/TB can manage without protectors is valuable, and thus would like an aliasing model in which the two are compatible.

18

I'm afraid I don't understand the problem statement. Obviously, the new memory must be somehow different from the old one, we want to enforce non-aliasing after all.

If LLVM adds support for "native allocators that may kill allocations with operations other than free", then I am not aware of any allocators that satisfy the Allocator contract that we could not optimize with SB/TB, including protectors. IOW, the StaticAllocator bound on the hypothetical NativeAllocator wrapper is temporary. This imposes limitations on users of the allocator (as documented here for the global allocator), though more fine-grained LLVM controls could lift many of them.

But I really don't see the fundamental issue with custom allocators you see with SB/TB. I agree there is a limitation with cell::Ref, that could be remedied by having a way to suppress protectors. And for self-referential generators my gut instinct is that we don't want the optimizer to touch them, but I could imagine that one can do better (but I wasn't able to reverse engineer a concrete example from your model that we'd like to be optimized, and I don't think it is fair to expect me to come up with motivating examples for your model -- or to expect me to try and understand a model without a motivating example to guide intuition). So, I concede alternative models could do better than SB/TB for those two points. But for Box, you really need to get more concrete in your description of the gap in prior work, though I cannot evaluate whether your model achieves that. Please give examples. The allocator in your issue is not an example, I am quite sure it would work fine if we actually had Refresh provenance of global allocator · Issue #2686 · rust-lang/miri · GitHub implemented (and the part that's missing is orthogonal to the aliasing model, it's about improving the model of "allocations" in Miri).

19

It is possible that I am overestimating what Box can do / is allowed to do. In order to clarify the sort of things I would expect it to be able to do, I wrote some example code that implements the mutable-borrow part of RefCell in terms of a custom allocator. It's probably a bit too long to post on IRLO, but is available on the playground.

It works as follows: MyRefCell contains a field storage: while the MyRefCell is unborrowed, it stores its internal value in storage; while it's borrowed, storage is used as memory backing the allocator. While it's borrowed, MyRefCell functions the same way as the allocator I wrote in my issue (with the only exception being that the allocator is a shared reference to the memory containing the allocation, rather than using a static variable), and while it isn't borrowed (meaning that storage is unavailable for allocating in), it always returns out-of-memory. I believe that this is (intended to be) a valid implementation of Allocator (and I think it even obeys the global allocator restrictions).

Borrowing the MyRefCell is done by moving the value out of storage, then using the MyRefCell as an allocator to create a Box that is necessarily allocated at storage's address; because the value is copied from an address to the same address (and all other memory accesses in between are provably disjoint), all this optimizes out and borrow_mut optimizes down into an assert that the MyRefCell is not already borrowed. When the borrow ends, it moves the value out of the Box, drops the Box, and moves the value back into storage; this pair of copies should optimize into memmove (which is likewise a no-op when moving a value onto itself), although for whatever reason LLVM seems unable to do that optimization and performs two copies instead.

I have been assuming that since RefMut isn't able to soundly use protectors, the Box<T, &MyRefCell<T>> in this program should likewise be unable to soundly use protectors, given that the code is (while somewhat convoluted) essentially equivalent to that of RefCell (and the pointers are set up in the same way as the current implementation). It's possible that there's some difference that I'm unaware of (or that RefMut could be made to work in the aliasing model using the same techniques that work for Box).

20

Thanks for writing up an example.

Note that ManuallyDrop suppresses special treatment of references and Box, so this will not get noalias treatment even if you use a global allocator. This was recently changed, finally fixing a long-standing footgun. But for the sake of discussion we can assume another type that works more like the old footgunny ManuallyDrop.

The key difference is that there is an explicit call to Allocator::deallocate that marks the end of the lifetime for this allocation. If you used Box<T, NativeAllocator<&'a MyRefCell<T>>> (if that was a thing), that call would destroy the provenance of the inner allocation and reconstruct the original pointer from the outer allocation (the one that Allocator::allocate returned). That should serve as an explicit barrier for how far down the compiler can move accesses to the noalias pointer, and that's why noalias should be fine here but is not fine with normal RefMut. These are the native allocator support operations I keep mentioning; I linked to Refresh provenance of global allocator · Issue #2686 · rust-lang/miri · GitHub often enough that I hope you had a look at it by now. :slight_smile:

Whether LLVM actually implements this interaction of noalias and allocator intrinsics correctly is a different question. :wink: