Disclaimer: As mentioned above, there is no decision yet on what the memory model should be. So I can basically only answer this by saying what Stacked Borrows has to say here, which as you noted is WIP, un-RFCed, and basically just my "hobby project". But it's also the best thing we got currently.
No. Lifetimes don't matter for the behavior of the program. They cannot, we erase lifetimes aggressively during compilation.
Very good question! The answer that I am proposing with Stacked Borrows is that the "lifetime" of the "borrow through the raw pointer" ends the moment the pointer from which it got created (x
in your case) gets "used" again. So in your example:
let mut x: u32 = 0;
let ptr: *mut u32 = &mut x; // "lifetime" of raw ptr starts
unsafe { *ptr = 5; }
x = 10; // "lifetime" of raw ptr ends
x
This is why the compiler is not allowed to reorder here.
Note that "use" is a fuzzy term, and currently Stacked Borrows considers many things a use. Hence this is UB:
let mut x: u32 = 0;
let ptr: *mut u32 = &mut x; // "lifetime" of raw ptr starts
let y = x; // x gets "used", so the lifetime of the raw ptr ends
unsafe { *ptr = 5; } // UB
x
It is. And certainly, in general, Miri is not in the state where we can guarantee anything like it detecting all UB.
However, your particular pattern seems to me like something any "reasonable" model would allow. I think a lot of code would break otherwis
While I am one of the maintainers of Miri these days, I wouldn't consider myself its "maker"; see the README for some more historic details.
Also, Miri is certainly a helpful tool, but shouldn't be used without consideration. So if after carefully thinking about your code you think you followed all the rules, and then you run it in Miri and Miri gives you a green light, then that's a good sign. But if you just do random stuff until Miri no longer complains, that's not verifying much of anything.
This is a great observation! I think it needs to be bold and italic:
Replacing references with pointers does not change if a program is sound.
I think this is a minimal standard we should require for any model. That's in fact kind of what I meant above by saying "any reasonable model would accept this code".