-
Notifications
You must be signed in to change notification settings - Fork 59
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Tree Borrows: Two-phase borrows + interior mutability have surprising interactions #501
Comments
Another way to put this is to say that actually, UnsafeCell does make a difference below mutable references -- specifically during the reservation phase of a two-phase borrows, UnsafeCell determines whether mutation through other pointers is allowed. |
Could we say that creating a protected tag via a Although this won't help if we make |
IIRC a bunch of things break in TB if we have tags that are activated without an associated write event. @Vanille-N might remember the details of that as I forgot... We could make function calls implicit writes for |
That's okay. If you hand out a raw pointer, you don't get any free aliasing model optimizations -- that's how it should be. |
If we allow activated tags without write events it breaks a lot of things indeed. In particular if we make that possible then
It should come to no surprise that these two assumptions are quite important. Compared to SB, Tree Borrows stops requiring implicit write on creation of |
The difference between this examples and the safe code "motivating example" for the weird behavior of interior mutable
So maybe we should somehow have it that when a protector on an item ends (i.e. the function into which it was passed as an argument returns), it also sets all But since there are two reborrows at play here (one inside the function, and one outside it in the parent function), you might also want to have a MIR |
Usually in SB and TB, we use conflicting memory accesses rather than static instructions to determine when borrows end. Intuitively, the two-phase ends when there is a write to the mutable reference. So ideally what would happen is that the Reserved mutable reference accepts foreign writes to interior mutable shared references, but not foreign writes to mutable references. Not sure if that's possible though? It would be a bit like saying we actually have two kinds of writes (statically annotated in the source, presumably), exclusive writes and non-exclusive writes, and writing to an |
FTR, by "activating new protecting tags" I was indeed suggesting an implicit write event. I'm hoping that by limiting it to protected tags, it wouldn't create too much extra UB. It seems like it would allow the aforementioned optimization (I also would like it for additional reasons, as it will make the relaxed version of the model saner to define) |
It would break code like this, which is code that we explicitly wanted to allow with TB: fn foo(x: &mut [i32]) {
let ptr1 = x.as_ptr();
let ptr2 = x.as_mut_ptr(); // implicit write invalidates `ptr1`
ptr2.copy_from(ptr1.add(16), 16);
} |
TBH, |
Tree Borrows makes implicit reads very harmless. That's one of the key advantages it has over SB. |
Turns out that this example is affected rust-lang/miri#3742. Now, the "leaking" of the |
if I write |
Yes, it relies on the other functions doing the proper retag. |
Consider this function:
If this was an
&mut i32
reference, then the*xr = ...
assignment would invalidate all child references and hence we could rely ondo_something
not being able to use anything derived from the reference passed toshouldnt_escape
.But it turns out under current Tree Borrows rules, that optimization would be wrong, as demonstrated by this example (due to @JoJoDeveloping).
The reason this works is that two-phase mutable references to
!Freeze
types in their reservation stage accept foreign write accesses. This is necessary to make code like this (entirely safe code!) not UB.This is probably undesirable. But I am not sure what the best way is to make the safe code example allowed but make the counterexample for the optimization above have UB.
The text was updated successfully, but these errors were encountered: