Stacked Borrows: An Aliasing Model For Rust

language design Unsafe Code Guidelines
33

The trouble with transmutes comes from having extra data stored at pointers, so there is a representation difference between mutable references, shared references and raw pointers. "Types as Contracts" had the explicit goal to not do that, so it did not have this problem.

However, it made lifetimes matter. I am not sure which is worse...

Then you are misunderstanding. My model explicitly performs "activation" of all references that enter or leave a function -- passed in as argument, passed out as argument, loaded from memory, stored to memory, passed in as return value, passed out via return. This gives us some nice invariants to work with -- it is needed, for example, for the dereferencable annotation. Also we do retagging on references coming in, we can't do that without looking at the data. The model is mostly access based, but not 100% so.

However, when doing "activation", I propose to not recurse through references. So for example, when a function receives (as incoming argument, incoming return value or loaded from memory) a (&mut i32, &mut i32), then these references are both activated. However, when it receives a &mut &mut i32, the inner reference is not touched at all. IOW, we look at the data coming in (two references in case of the pair, one reference in the second example), but we do not go into memory to perform some recursive action.

I do not understand how you are counting references. The second line is a raw-ptr-to-shared-ref, so it will do the following to all locations "covered" by the ref -- the ref has type &(&i32, &i32), so that would be 16 locations (with 8 bytes pointer size):

  1. Activate a Raw (so some_address must be frozen or have a Raw in the stack)
  2. Bump the clock and assign the newly created shared ref the current timestamp.
  3. Initiate Frz(current_time), which will freeze the location.

The values stores in these locations (which happen to be references again in this case) do not matter at all here.

Yes. Let's look at the most important steps happening:

    unsafe {
        (*a).next = &*b; // <--
        (*b).next = &*a;
        &*(a as *const Node)
    }

At the marked line, we create a shard ref covering whatever memory b is stored in. This follows the steps I described above, so in the end, that memory is frozen. In the next line, b.next is mutated again, which is okay because there is a Raw in the stack -- but will end the freezing for that part of memory (the last 8 bytes of b), because you cannot mutate something frozen.
Finally, later a.next.next aka b.next is accessed. This will activate that shared reference, asserting that memory is still frozen -- triggering UB because memory is in fact not frozen any more.

Taking a step back, at (*a).next = &*b; you are creating a shared reference. That is a promise that the memory pointed to by this reference will never be mutated while this reference is valid. The reference points at wherever b sits in memory. The next thing you do is mutate b. The only way now to maintain your promise is if we say that this invalidate the reference you just created. (With types as contracts, btw, this would already be UB -- types as contracts takes lifetimes into account, so the moment you create an &'static pointing at something, that memory is marked as read-only forever. Which makes sense, because that's literally what &'static is.)

We have to find a way to make this work without mutating memory pointed to by a shared reference. One way is to opt-out of the promise I mentioned above by using Cell or UnsafeCell. So if you replace &'static Node by Cell<&'static Node> or UnsafeCell<&'static Node>, you should be good. Would that be an acceptable solution? It changes the type throughout the program, but it also reflects better the fact that the memory here is being mutated while there is a shared ref pointing at it.

1 Like