This probably seems like a strange question, but I've noticed that the borrow checker doesn't support strong updates and I'm wondering whether there is some subtle reason for this I'm not aware of. Specifically, this example doesn't compile:
fn test() -> i32 {
let mut x = 1;
let mut y = 2;
let mut p = &mut x;
// p |-> x
let mut q = &mut p;
// p |-> x, q |-> p
*q = &mut y;
// p |-> y, q |-> p
x + *p
}
This seems to me like it should be fine, since the borrow checker could (in principle) reason that, after the indirect assignment through q, the borrow of x has ended. Indeed, if we replace *q = &mut y with p = &mut y then it's fine as expected.
How does this come up in real code? All the cases I can imagine are either a) contained within a single function like this, where it's both easy and preferable to only ever borrow x and y directly, or b) split across multiple function boundaries so the borrow checker would not be allowed to make this sort of inference.
(also, why "strong" updates? What's stronger about this than any other kind of update?)
Well, it hasn't come up specifically that I'm aware of. I am attempting to formalise the semantics of Rust and found this discrepancy from what I imagined.
The term strong update comes from the static analysis community, where it is often used in the context of pointer analysis (which is somehow similar to what's going on here).
Simplistic TL;DR of the Stacked Borrows work: formalize the borrowing memory model that applies to all code, even code that uses unsafe, must abide by. As it works with raw pointers as well, it deals exclusively in "uses" of borrows, not the (NLL) regions in which they are "live". And as such, the static borrow checker is a strict subset of what is allowed in the memory model, but that's ok; that's why we have unsafe: to model borrowing rules that are allowed by the memory model but not by the Safe Rust subset.
Thanks for that. But I am more interested in the answer to my question at this stage. I'm guessing roughly speaking the answer is: Rust doesn't support this, but it could. There's no compelling reason to at this stage.
You might also be interested in Polonius, which is an experimental more formal implementation of the static borrow rules.
In terms of Stacked Borrows's model of the borrowing rules, this would be allowed (as far as I can tell, anyway). However, I think the safe lifetimes cannot support this, due to how lifetime typing works. Roughly explaining as polonious-style borrow regions:
let mut x = 1; // open region 'x
let mut y = 2; // open region 'y
let mut p: &'p _ = &'0 mut x; // open region 'p; 'x > 'p
let mut q: &'q _ = &'1 mut p; // open region 'q; 'p > 'q
*q = &'p mut y; // uses region 'p; 'y > 'p
// end region 'q
// note: at this point, 'p is holding access to 'x and 'y
// 'x or 'y cannot be used without first ending 'p
// this is required because a region does not change what regions it locks
x + *p; // Illegal; need to end 'p to use x,
// but then use 'p afterwards
*p + xmight be allowed with Polonius, if it allows ending borrow regions within an expression. But 'p will always require locking both 'x and 'y, because any binding only has one type and (up to) one associated region, and those aren't changed by assignment.
Yeah, I have been looking at Polonius. But, am not sure how to use it to answer my question.
Its interesting that you believe StackedBorrows supports this, and yet Rust itself doesn't. I guess the question is: should we expect Rust to support it at some point?
Stacked borrows is a runtime model about what is allowed. The borrow checker will always be an approximation of this unless you solve the halting problem:
let mut a = Box::new(0);
let b = a.as_ptr();
drop(a);
potentially_not_halting_operation();
unsafe { *b = 1; }
Is allowed under stacked borrows if potentially_not_halting_operation() doesn't halt. The borrow checker can't prove if it does at compile time, so it has to reject it.
This isn't related to the discussion so far, but I think it's worth noting that your example isn't minimal. Even completely removing all code involving q, it fails to compile:
fn test() -> i32 {
let mut x = 1;
let mut y = 2;
let mut p = &mut x;
x + *p
}
Rust isn't complaining about your use of q as a borrow to p, it's complaining solely about that last statement there. Specifically, you use x while p still exists.
Expanding the code, you have something like
let mut x = 1;
let mut p = &mut x;
// p |-> x
let _temp1 = x;
// p |-> x
let _temp2 = *p;
// p's borrow can now end
(_temp1 + _temp2)
The thing that's being complained about is that p lasts all the way through the *p expression, and thus it holds its borrow over x that long. You can't use x while p still exists and will be used at a later time.
If you replace x + *p with *p in your original example, or with *p + x, it compiles fine.
Could you confirm which exact error you're talking about rust possibly supporting? Or, more directly, whether you intended the interaction between p and q to be the center of your post, or for this interaction between x and p?
Either way, I think a more minimal example could help convey the point! Analyzing rust code is hard, and telling exactly what an error about is made harder the more code is present (even a few extra lines can confuse someone - I originally thought the error was about q borrowing from p until I tried to mess around with it more to test what exactly was going wrong).
You seem to have missed the point. Pay attention to this sencence:
This doesn’t apply to your supposedly minimized example anymore. In fact, OP is probably very aware of the fact that x + *p uses x while p is still alive, that’s as far as I can tell why OP used this expression in the first place, and it is not OP’s point that this might be changed to be accepted by the borrow checker. The only redundant thing I can see here is the use of numbers, the return and the addition (and the mutability of q), so an actually minimized example might be:
fn test() {
let mut x = ();
let mut y = ();
let mut p = &mut x;
// p |-> x
let q = &mut p;
// p |-> x, q |-> p
*q = &mut y;
/* ^^^^^^^^^^^ replace this line with
p = &mut y;
and the program will now compile even though
it still does the same thing (because q points to p)
*/
// p |-> y, q |-> p
x; // access x while
p; // p is still alive
}
Thanks for the discussion on this so far. A few points:
Rust isn't complaining about your use of q as a borrow to p , it's complaining solely about that last statement there.
Right, as steffahn points out, this isn't what I'm getting out. The point is that the statement *q = &mut y; doesn't terminate the borrow of x, even though this is actually what happens here. The statement p = &mut y however does terminate the borrow of x.
I appreciate what you are saying, however in this case we don't need to solve the halting problem to resolve this issue. In theory at least, it would be pretty easy for the borrow checker to spot this and act on it. Of course, in practice, the particular design of the borrow checker may make this harder than expected. And, as was pointed out, the Polonius work may offer some new opportunities.
Don't think it makes sense to add an analysis for this unless this is a pattern that is useful in real code, which seems unclear, because if the compiler can determine that q points to p, then the programmer should just write "p = " instead of "*q = ", and also if p is always going to be reassigned, then there is no need to have it point to x in the first place.
I feel like we've been too subtle in the existing replies and missed the big disconnect here.
As far as I know there are no complete formal semantics for just the current "borrow checker" in isolation from the rest of the language, because:
it's still heavily evolving, and that evolution is motivated largely by what "could-be-safe" code users complain about in practice, versus how expensive it is to validate it on every single compile
Modern borrow checking is pretty much defined on MIR, and there are many more reasons why MIR itself is evolving and unlikely to be stabilized in the forseeable future (maybe ever?)
"formalizing Rust semantics" usually means formal semantics for all of Rust, including unsafe code (since most of the potential benefits of formalization don't apply otherwise). At that point, what the borrow checker chooses to allow in safe code is a relatively uninteresting subproblem, because any "could-be-safe" / non-UB code is already writable with raw pointers.
3 is why all of the Stacked Borrows documentation only talks about the borrow checker for the purposes of proving that "safe Rust" is a strict subset of "UB-free Rust" according to Stacked Borrows.
For 1, the simple fact is that the "strong update" case you describe has never been a significant pain point for Rust users, which is what I was trying to get at earlier with:
So although it's probably straightforward to add support for this, it's unlikely to be worth the costs (largely in compile time, but also in making it harder to understand what the compiler will or won't accept). Yes, I'd expect those costs are relatively small in this case, but we're talking about small cost vs miniscule benefit.
For examples of cases which have caused many Rust users pain, such that we have/are/will be investing a lot of effort into solving them, see the 4 "problem cases" in the NLL RFC (I believe 3/4 are now accepted on stable these days?), and for more details/history/future plans see every @nikomatsakis blog post in the "NLL" category. In particular, the URLO thread for his "After NLL" post discusses ideas like "borrow views" in great detail, yet IIRC no one there requested "strong update"/"flow-sensitive" borrow checking.
Regardless: if you just want to formalize some version of Rust's borrow checker behavior as a starting point for other work, without worrying about exactly matching the current or future state of actual stable Rust, then I'd recommend using the description in the NLL RFC. I'm fairly sure it's not an exact match to any past/present/future version of actual stable Rust, but AFAIK it's by far the most thorough and self-contained description of a Rust-like borrow checking algorithm we've ever published.
In fact, IIRC, the borrow checker doesn't even fully implement the NLL RFC, and there are other potentially sound relaxations like 2-phase borrows that have not been stabilized yet because they may require breaking changes or more design work or both.
As others have noted above, the borrow checker doesn't try to necessarily have some sort of formally-specified semantics. Rather, its design has been mostly based on finding common papercuts that users have and that are actually safe (e.g. see the examples in the NLL RFC) and making the borrow checker smart enough to allow them. This has been done with much discussion and deliberation and testing because once we choose to allow some code, our stability guarantees force us to keep allowing it. In the latest iteration, a major implementation choice was made to move from an AST-based analysis to a MIR-based analysis, enabling NLL and thus solving a bunch of common annoyances.
The compiler has to make a tradeoff between being smarter about borrow checking vs compiler performance and implementation complexity. NLL was judged to be a big enough improvement that it was worth the implementation changes and performance regression. Hypothetically, we could start accepting the pattern that you proposed in the OP too, but it would need to be justified with data showing that supporting such a pattern is worth the added performance and implementation costs. So far, nobody has produced such evidence, so the borrow checker has never implemented them.