Closed nikomatsakis closed 5 years ago
The key point is that
TMP2 = &mut2 foo.as<Some>.0
is a 2-phase borrow that never gets activated.
The "never gets activated" is important, because this blatantly overlaps with a shared borrow. So this is like an "immutable &mut
". And the only reason we have it is that we want an & &mut T
(the only use of TMP2
is TMP3 = &TMP2
).
So yeah, the proposal is to instead create that &&mut T
directly from an &&T
, which is a safe conversion.
@RalfJung yep, reworded to make that a touch more explicit
I thought we were using TMP2
as x
(i.e. the match binding) both inside the arm and inside the guard, but apparently we don't and the world doesn't explode.
However, having x
be the same both within the guard and outside it means that x
maintains a single consistent address during its lifetime, so e.g. this code always prints the same address twice (which I think is the right thing to do, but of course we can specify it either way).
#![feature(nll)]
fn main() {
let mut x = 2;
match x {
ref mut t if {
println!("In Guard: {:?}", (&t) as *const &mut i32);
true
} => {
// with current play.rust-lang.org debug, this prints a different address
// than in the guard.
println!("In Arm: {:?}", (&t) as *const &mut i32);
}
_ => {}
}
}
For a less "cosmetic" problem, I don't see how the proposed lowering would handle array indexes that might not be disjoint (and potentially similar cases involving unions). We can't rewrite x[j]
to be a function of x[i]
because it isn't.
#![feature(nll)]
fn main() { doit(0, 0); }
fn doit(i: usize, j: usize) {
let mut x = [Vec::new(), Vec::new()];
x[i].push(x[j].len());
}
I think the "array access" problem is currently a bit "academic", because accessing things like Vec<T>
involves calling Deref
which loses the "purity magic", but it will become a bigger problem come DerefMove
.
With DerefMove
, couldn't we detect the "root" of what is being referenced, and then rewrite that? So with x[i].foo(x[j])
, we'd rewrite x
.
Rewrite x
to what?
If we also allow for "complex" cases like x.a[i].foo(&mut x.b, x.a[j])
, this rewriting starts feeling like reimplementing the borrow checker in the lowering.
In any case, why is DerefMove
a required ingredient? You can't move from something that is borrowed.
In addition to these "rewriting is a PITA" issues, there's also a more "fundamental" way to differentiate rewrite-based from "real 2-phase based" approaches: 2-phase borrows allow pre-existing immutable borrows to live right up to the activation point, as in:
fn main() {
let mut x = vec![];
let p = &x;
x.push(p.len());
}
Unlike the previous examples which seem like a very natural combination of features, I'm less sure that this has to work to "not be a bug in 2ΦB" - either way would be "fine".
Rewrite x to what?
x[i].foo(x[j])
becomes
let tmp = &mut x;
let x2 = &*tmp;
let _1 = x2[j];
tmp[i].foo(_1)
but yeah, once we want to do this for more complex paths (in particular, once there are disjoint paths) this becomes more "interesting". x.a[i].foo(&mut x.b, x.a[j])
we could handle by saying "we apply the rewriting based on the path before the first Index
", but that might fail otherwise.
In addition to these "rewriting is a PITA" issues, there's also a more "fundamental" way to differentiate rewrite-based from "real 2-phase based" approaches: 2-phase borrows allow pre-existing immutable borrows to live right up to the activation point, as in:
Yeah, this will never be as powerful as "full" 2-phsae borrows.
Funny enough, I find your example actually easier to think about in terms of my RustBelt model of types that x.push(x.len())
. Namely, after
let mut x = vec![];
let p = &x; // let's call this lifetime 'a
there is something you have in your typing context (we called it a "blocked type assignment") which says that once 'a
is over, you get full permissions for x
back. All two-phase borrows would do here now is to change this to
x
is shared for 'a
(we would need for for other stuff as well), and&mut x
(part of the method call) have the effect that x
changes to "once 'a
is over, you have a mutable borrow to x
" -- essentially "chaining" the proof that from owning x
we can create a mutable borrow together with the blocked type assignment for x
.Obviously I haven't worked this out in all details, but it seems at least plausible. I would then also think the same way about x.push(x.len())
: We first create a shared reference and obtain a blocked type assignment for x
, and then we do the &mut x
for the first parameter of push
.
Now what does this mean for stacked borrows? I suppose it means we would allow creating a &mut
for a frozen location as long as it does not get activated.
@RalfJung @arielb1
but yeah, once we want to do this for more complex paths (in particular, once there are disjoint paths) this becomes more "interesting".
x.a[i].foo(&mut x.b, x.a[j])
we could handle by saying "we apply the rewriting based on the path before the firstIndex
", but that might fail otherwise.
Note though that we don't currently handle examples involving Deref
or Index
. My assumption has been that if we want to handle things like Index
trait, we are going to have to go to something more like @arielb1's Ref2 — that is, a more fundamental expansion of what a lifetime is. In particular, I think we need to trace those results through the type.
This is however the largest source of regressions (aka bugfixes). Most of them have the form of something like vec[i] += vec[j]
, though sometimes it is something like foo(&mut bar, bar.baz())
. It may or may not be something we wind up wanting to fix.
Another thing to consider: how the Polonius model comes into play here. Until now, Polonius and 2-phase were orthogonal. I had expected to transition the existing codebase to use Polonius once we "ship" — something which, actually, gets a lot easier if we do the rewriting-based approach we are talking about here — but maybe it's worth thinking about how we can model something like 2-phase there as well. (That .. doesn't seem too hard. In particular, I could imagine threading a kind of "Activated" fact along.)
The borrow-checker (both the AST and NLL borrow checkers) also has the weird feature where it lets you concurrently borrow separate fields of indexes of an array (which is sound whether the indexes are the same or not):
fn main() {
let mut x = [(1,2),(2,3),(3,4)];
let (i, j) = (0, 0);
let a = &mut x[i].0;
let b = &mut x[j].1;
std::mem::swap(a, b);
}
There's no obvious way of handling
let p = &x[i].1;
x[j].0.f(*p, x[k].0.len());
We have to decide whether to mutably borrow x
or x[j].0
. If we mutably borrow x
, then we break p
(which does conflict with today's AST borrow checker, even if nobody uses it in practice), and if we mutably borrow x[j].0
, we can't redirect x[k].0
.
I'm not sure how many people use this (especially intentionally). The solution might be to remove the feature entirely. I don't like having a situation where we sometimes borrow x
(breaking p
) and sometimes borrow x[j].0
(not breaking it) depending on "irrelevant features of the program".
These sort of things make me wary of having a MIR-rewriting solution.
In a recent Zulip chat, @nikomatsakis also noted this example (where the receiver of a method call is "potentially modified" by the subsequent evaluation of the expressions for the actual arguments to the call):
@pnkfelix on the topic of implementing 2PB via rewriting, I see that this example compiles:
fn main() { let mut x = &mut vec![]; let mut y = vec![]; x.push(( { if false { x = &mut y }; 22 }, x.len(), )); }
though I suspect that this one doesn't occur a lot in the wild =)
I think deciding the question (of whether we want to allow this change #53198) effectively blocks any final resolution of #46901.
Thus, in terms of #56754: given that #46901 is P-high, I am going to likewise tag this as P-high (just in terms of resolving whether we are going to do this, or not).
@Centril notes on Zulip:
it seems like T-lang should be brought in at some point before any irreversible action is taken (e.g. changing semantics in a user observable way or finalizing documentation)
I've started to lean against this "do it in MIR lowering" approach. The example of a "potentially modified" variable convinces me it is too complex to be worthwhile -- how would we know when to rewrite the x
in the x.len()
there? We'd need dataflow analysis or something to do that.
Agreed. Also, the current implementation of 2PB in Miri shows that a subset of them (see #56254) can be explained with a very small extension of the aliasing model. That doesn't mean that it'll be easy to add that to LambdaRust or so, but it shows that at least on the level of Stacked Borrows, we can explain a subset of 2PB as just "shared reborrow of the mutable borrow" without having to rewrite anything.
The reason this works is that in Stacked Borrows, once a mutable borrow got shared-reborrowed, for doing read accesses it does not matter whether you are using the mutable borrow or one of the shared reborrows, they all behave the same and can be used interchangeably. In the case of 2PB, the mere existence of a shared reborrow thus suffices to explain this subset of 2PB.
Given the various comments, I'm going to close this issue. Remaining discussion can focus on #56254.
@RalfJung and I were talking and we realized that -- with a bit of work -- we could make 2-phase borrows be something fully handled during MIR lowering. This is nice because it means that the rest of the model (e.g., the Unsafe Code Guidelines aliasing model) doesn't have to be aware of it.
There are basically two places we use 2PB today. Let me break down at a high-level how to handle each of them.
Method calls, operators, etc
The first place is for a case like
self.push(self.len())
. Today, we lower to thepush
call to:The borrow checker finds the use of TMP0 on the last line and considers that the activation point. In particular, for each 2PB, there must be an exactly one use which is dominated by the borrow and which postdominates the borrow. This use is the activation point.
The idea would be to change to instead lower as:
Here, we borrow
self
mutably as normal but then reborrow it to create a shared referenceTMP1
. Then, when we lower the arguments, any reference toself
is rewritten so that it does not refer toself
but rather*TMP1
(which has the same type asself
). Then the normal NLL mechanisms come into play.We'd obviously have to tweak our error messages here so that
*TMP1
is displayed as "self" to the end-user.*The key observation here is that we can statically see all references to
self
while lowering the arguments and rewrite them to reference `TMP1` instead.** (In fact, we already use a mechanism like this when lowering match guards, see below.)Matches
We also rely on 2PB to handle variables in match pattern guards. The basic idea of how we lower something like this:
is that we introduce various artificial borrows. The first is a borrow of the place being matched (
foo
) -- that borrow begins when the match begins and ends upon entering some arm. The second is for bindings that are accessed during match arms. These are each implicitly mapped to a dereference of a shared borrow. So (today!) you wind up with something like:Again, this is what we do today. For this to work, we rely on
TMP2 = &mut2 foo.as<Some>.0
being a 2-phase borrow that never gets activated, since otherwise it would overlap with theTMP0
borrow that is definitely still in scope.Instead of that, we will create a shared borrow and then use some kind of case from
&&T
to&&mut T
:This cast is provably safe (@RalfJung has done it!), so there is no unsafe code or anything else involved here.
cc @pnkfelix @arielb1
UPDATE: Lightly edited for clarity.