Comment by Arnavion
3 days ago
Stacked borrows is miri's runtime model. Run it under miri and you will see the error reported for the `*x = 10;` version but not the `write(x);` version - "Undefined Behavior: attempting a write access using [...] but that tag does not exist in the borrow stack for this location".
rustc itself has no reason to reject either version, because y is a *mut and thus has no borrow/lifetime relation to the &mut that x is, from a compile-time/typesystem perspective.
Ah that make sense. Thanks for clarifying.
The paper mentions that the authors implemented tree borrows in Miri. Is this change likely to be adopted by Miri as the default model going forward?