Inconsistency between stacked borrows and my mental model

So I was reading the Stacked Borrows Implemented blog post, and realized that the following is not considered UB by stacked borrows:

fn main() {
    let x = &mut 1u8;

    // Create raw pointer
    let y = x as *mut u8;

    // Assert uniqueness of x
    *x = 7;

    // Create another raw pointer
    x as *mut u8;

    // Read x through y, which was created before we asserted uniqueness.
    let _val = unsafe { *y };


I found it really surprising that reading through y is not considered UB here, because in my mental model, y would have been invalidated by asserting uniqueness with the write.

Note that if you remove the immediately-ignored raw pointer, miri will complain. I don't have any questions, I just found this surprising and wanted to share it.


I asked about a vaguely similar case in this Zulip thread, where @RustyYato and @RalfJung replied:

Yato: Yes, all raw pointers have the same tag (which is untagged) right now, so making a new raw pointer to the same location revives old raw pointers incorrectly.

RalfJ: note however that to match what LLVM does with noalias , we need to eventually also track raw pointers better and then that kind of code would stop working

So I believe this is a known limitation of the current Stacked Borrows model which might be changed in future revisions.


Exactly. :slight_smile:

1 Like

This topic was automatically closed 90 days after the last reply. We invite you to open a new topic if you have further questions or comments.