Stacked Borrows: An Aliasing Model For Rust

[RalfJung]

@jpetkau

Here’s short example that just creates a cyclic linked list, and a longer one that actually deserializes a graph.

Thanks, this helps a lot!

As @gereeter wrote, this code is UB:

    let a: &'static mut Node = alloc(Node {
        name: "a",
        next: &EMPTY,
    });
    let b: &'static mut Node = alloc(Node {
        name: "b",
        next: unsafe { &*(a as *mut Node) },
    });
    a.next = b;

You are creating a shared reference to a, and then mutating it. I think allowing this would inhibit most of the optimizations we want to do around shared references.

UnfinishedNode with an UnsafeCell is one possibility to get around this. Another one might be to use raw pointers, though transmuting a raw pointer to a shared reference is also somewhat subtle...

@jpetkau

the lifetime (in the “define what’s UB sense”, not the static checker sense) of the reference created on line 31 ends immediately, since it’s never actually used. It is reachable from another reference but it’s never actually reached . (And we can’t outlaw the mere existence of a chain of references that would point to mutating memory if someone were to follow them, because there are plenty of totally safe ways to do that.)

Then the ‘launder’ on line 37 discards all the old references and creates a fresh one, so the compiler can’t assume anything about (transitive) loads through it from before line 37.

The launder does not affect the data behind the reference though -- it launders the outer & in &'static Node, but it does not have any effect on the references stored inside that struct.

And if it did, the a as *const _ -- casting a shared ref to a raw ptr -- will activate the source reference, so it is like a use.

@jpetkau

The model that fits my intuition is analogous to data dependent reads in a processor memory model,

Oh, data dependency models are usually pretty much impossible to use for a source language. (E.g.: does x * 0 depend on x?)

@jpetkau

When a ref is created by loading through another ref, it gets the parent ref’s timestamp.

This is an interesting suggestions. I find it a bit odd, TBH -- I'd expect it to maintain its own timestamp. But I think one could adapt my model just a tiny bit to have a very similar effect (otherwise it already seems to have a lot in common with yours): When a shared ref is loaded, we don't activated it -- we just retag (give it a new timestamp and initiate that). You would probably want to do the same for mutable references.

My intuition was that you would want the ref you load to already "have been valid".

However, this might not interact too well with the barrier... not activating the reference being loaded means that it might actually not be derived from the parameter... for example

fn foo(x: &mut i32, z: usize) -> i32 {
  *x = 12;
  let y : &mut i32 = bar(usize); // imagine this aliases x
  *y = 13;
  *x // can we optimize this to 12?
}

Under a model that doesnt activate incoming references, y might actually push its own Uniq on top of x, and then later when x is used again that gets popped. So the above could would be allowed. That does not seem right to me.

So, I am not sure I like "loading a ref inherits the parent timestamp". This makes it completely irrelevant where the loaded ref is coming from, i.e., how it was computed; that's a lot of information that would go missing. Maybe it works if we do this only for shared references, I would have to think more about that.

@jpetkau

An unrelated observation (I made it earlier but now realize that it applies more broadly). For owning types like Rc<T> , Vec<T> and especially Box<T> - if you start with an immutable root, the whole graph is immutable, and the compiler should be able take advantage of that just like with plain refs. But the model falls back to the free-for-all ‘raw pointer’ case because they these types use pointers in their implementation. Does this inhibit possible optimizations or sanitizer checks? (If so, maybe special rules for std::ptr::Unique would fix that?)

The compiler should understand that things are immutable once the & surfaces. Before that, I find it hard to communicate this intent -- but yeah, maybe there is a way to make Unique mean something. I am not sure what it would mean, though.