Stacked Borrows: An Aliasing Model For Rust

language design Unsafe Code Guidelines
12

Looks good.

I’m somewhat concerned about how barriers interact with cases where lifetime disjointness is enforced by dynamic checks. Let’s take your demo code, which you explained would be UB if x and y point to the same location:

fn demo5(x: &mut i32, y: usize) -> i32 {
  *x = 42;
  foo(y);
}

fn foo(y: usize) {
  let y = unsafe { &mut *(y as *mut i32) };
  *y = 7;
}

But then change &mut i32 to RefMut<i32>, and usize to &&RefCell<i32>:

use std::cell::{RefCell, RefMut};
use std::mem::drop;

fn demo5x(mut x: RefMut<i32>, y: &&RefCell<i32>) {
  *x = 42;
  drop(x);
  foo(y);
}

fn foo(y: &&RefCell<i32>) {
  *y.borrow_mut() = 7;
}

fn main() {
    let x = RefCell::new(42);
    demo5x(x.borrow_mut(), &&x);
}

This is now entirely safe code. But from your borrow model’s perspective, it ought to be equivalent:

  • RefMut<T> contains &mut T as a field.
  • &RefCell<T> is a shared reference with interior mutability, which in your model behaves like a raw pointer (using a Raw item). The double reference (&&RefCell<T>) is so that retagging doesn’t take effect, i.e. neither demo5x nor foo will push another Raw on entry.
  • I had to explicitly drop the RefMut, but that shouldn’t affect anything; it only writes to the RefCell's state field, not the value itself.

So this should also be UB. Am I mistaken?

1 Like