[nll] move 2-phase borrows into MIR lowering

@RalfJung

@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 the push call to:

TMP0 = &mut2 self
TMP1 = lower<self.len()>
push(TMP0, TMP1)

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:

TMP0 = &mut self
TMP1 = &*TMP0;
TMP2 = lower<self.len() where self=*TMP1>
push(TMP0, TMP2)

Here, we borrow self mutably as normal but then reborrow it to create a shared reference TMP1. Then, when we lower the arguments, any reference to self is rewritten so that it does not refer to self but rather *TMP1 (which has the same type as self). 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:

match foo {
  Some(ref mut x) if G => ... 
}

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:

// Start of match
B0 {
  TMP0 = &foo // the match borrow
  TMP1 = DISCRIMINANT(foo)
  if TMP1 == Some { goto B1 } else { B3 }
}

// We found `foo` is a `Some`
B1 {
  TMP2 = &mut2 foo.as<Some>.0
  TMP3 = &TMP2
  TMP4 = <lower G where x=*TMP3>
  if TMP4 is true { goto B2 }
}

// Corresponds to the `Some` arm:
B2 {
  DROP(TMP0) // borrow of `foo` ends as we enter the arm
  <lower arm body>
}

B3 { ... }

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 the TMP0 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:

B1 {
  TMP2 = &foo.as<Some>.0
  TMP3 = &TMP2
  TMP4 = TMP3 as &&mut T
  TMP5 = <lower G where x=*TMP4>
  if TMP5 is true { goto B2 }
}

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.

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

@RalfJung yep, reworded to make that a touch more explicit

The match lowering - we currently break address consistency

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);
        }
        _ => {}
    }
}

The method lowering - array accesses

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

Also remember in that blocked assignment that x is shared for 'a (we would need for for other stuff as well), and
make that &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

@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 first Index", 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.

@nikomatsakis

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

@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.

Navigation Menu

Repository navigation

[nll] move 2-phase borrows into MIR lowering #53198

Method calls, operators, etc

Matches

The match lowering - we currently break address consistency

The method lowering - array accesses

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

[nll] move 2-phase borrows into MIR lowering #53198

Description

Method calls, operators, etc

Matches

Activity

RalfJung commented on Aug 8, 2018

nikomatsakis commented on Aug 8, 2018

arielb1 commented on Aug 11, 2018

The match lowering - we currently break address consistency

The method lowering - array accesses

arielb1 commented on Aug 11, 2018

RalfJung commented on Aug 13, 2018

arielb1 commented on Aug 17, 2018

arielb1 commented on Aug 17, 2018

arielb1 commented on Aug 17, 2018

RalfJung commented on Aug 21, 2018

nikomatsakis commented on Aug 22, 2018

arielb1 commented on Nov 28, 2018

pnkfelix commented on Dec 21, 2018

pnkfelix commented on Dec 21, 2018

pnkfelix commented on Dec 21, 2018

pnkfelix commented on Dec 21, 2018

nikomatsakis commented on Jan 3, 2019

RalfJung commented on Jan 4, 2019

nikomatsakis commented on Jan 4, 2019

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions