Non-lexical lifetimes draft RFC + prototype

[nikomatsakis]

New blog post:

http://smallcultfollowing.com/babysteps/blog/2017/07/11/non-lexical-lifetimes-draft-rfc-and-prototype-available/

I’ve been hard at work the last month or so on trying to complete the non-lexical lifetimes RFC. I’m pretty excited about how it’s shaping up. I wanted to write a kind of “meta” blog post talking about the current state of the proposal – almost there! – and how you could get involved with helping to push it over the finish line.

TL;DR

What can I say, I’m loquacious! In case you don’t want to read the full post, here are the highlights:

• The NLL proposal is looking good. As far as I know, the proposal covers all major intraprocedural shortcomings of the existing borrow checker. The appendix at the end of this post talks about the problems that we don’t address (yet).
• The draft RFC is available in a GitHub repository:
  • Read it over! Open issues! Open PRs!
  • In particular, if there is some pattern you think may not be covered, please let me know about it by opening an issue.
• There is a working prototype as well:
  • The prototype includes region inference as well as the borrow checker.
  • I hope to expand it to become the normative prototype of how the borrow checker works, allowing us to easily experiment with extensions and modifications – analogous to Chalk.

[arielb1]

Nice to see that 3-point error messages end up so well! I remember there was some case where inference did end up non-linear (which would mean that we would get some “spurious” 3-point errors that can’t actually occur even if we ignore control flow), but I don’t remember exactly when. I should write up the “formal” fixed point rules, at least on paper.

That might not be a problem in practice, but there might be some annoying examples on which we would give non-obvious error messages.

A few comments on details:

Diverging Functions

One interesting thing with the new algorithm, is that if we have a function that loops endlessly with no potential of panics, the StorageDead for locals can get deleted, and we can treat them as &'static references:

fn foo(p: &mut &'static u32) {
    let x = 2;
    let z : &'static u32 = &p;
    loop {
        *y = p;
    }
    // the `StorageDead` for `z` is unreachable, so no borrowck conflict with anything
}

In current Rust, I don’t think you can do any communication without the possibility of panics, so that is a bit of a useless curiosity, but if we e.g. made intrinsics not have an unwind edge before borrowck, this might allow some “interesting” patterns.

Additionally, there’s a potential practical problem - ATM we don’t emit StorageDead on unwind paths, and that might actually be observed by code (that also means that if we want to avoid major unsoundness, we need to regard the resume terminator as being a StorageDead of all locals):

struct NoisyDrop<'a>(&'a mut u32);
impl<'a> Drop for NoisyDrop<'a> { /* .. */ } // not blind to anything

fn foo() {
    let x;
    let mut y = 0;
    x = NoisyDrop(&mut y);
    loop {
        maybe_panic();
        // again ^, there's no `StorageDead` for `y` inside `foo` to conflict with
        // its borrow.
    }
}

As a fix, we might want to emit the StorageDeads and later on remove them during pre-translation (to avoid landing pad pessimization).

Free regions are always alive, even in hairpin loops

A more “region-inferency” example to the previous one, that shows that we must treat free regions as alive in all cases, and not just at function return points (that’s more of an “implementation issue”, but it is something to be aware of).

fn foo<'a>(d: &'a mut Result<fn(), usize>) {
    fn innocent() {}
    *d = Ok(innocent);
    send_to_other_thread(d);
    loop {
        *d = Err(0x6861636b65642100);
    }
}

[arielb1]

And the nonlinearity I wanted - not sure how serious it is:

// if either of the assignments in blocks X/Y are removed, the
// code compiles, so this code is sound, but does not compile
// with the current version of NLL inference.

struct Foo {}

let foo: Foo;
let a: &'a mut &'aa mut Foo;
let b: &'b mut &'bb mut Foo;
let c: &'c mut &'cc mut Foo;

block START {
    a = use();
    b = use();
    c = use();
    foo = use();
    goto X Y;
}

block X {
    b = &'b mut *a;
    goto END;
}

block Y {
    c = &'c mut *b;
    goto END;
}

block END {
    *a = &'a mut foo;
    use(b);
}

[nikomatsakis]

And the nonlinearity I wanted - not sure how serious it is:

Sorry, can you expand on this a bit more? I don’t quite get why this example is problematic yet.

Maybe I don’t understand it, but I’m not quite seeing the behavior this comment describes:

// if either of the assignments in blocks X/Y are removed, the
// code compiles, so this code is sound, but does not compile
// with the current version of NLL inference.

In particular, removing the assignment from the block Y does not make the error go away. Removing the assignment from the block X does, but that doesn’t seem surprising, since it is directly involved in the error.

Put another way, there is a path (X/0, X/1, END/0, END/1) in which *a gets borrowed to make b (at point X/0), modified through the original path *a (END/0), and then the reference b is used (END/1). That seems like it should be an error, no?

Am I missing something obvious?

Oh, one other thing: you used 'a both in the type of a and as the region of the borrow in END. I don’t think we would ever do that for real – rather, we would make the lifetime of each individual borrow be a fresh region variable (i.e., '_). Not sure if that affects things (I seem to get the same errors either way.)

[arielb1]

Ignore this. It does not work. Must have been me making a mistake or something…

[nikomatsakis]

Additionally, there’s a potential practical problem - ATM we don’t emit StorageDead on unwind paths, and that might actually be observed by code (that also means that if we want to avoid major unsoundness, we need to regard the resume terminator as being a StorageDead of all locals):

Remind me why we don’t put StorageDead for unwinds again? I wanted to ask about that.

As a fix, we might want to emit the StorageDeads and later on remove them during pre-translation (to avoid landing pad pessimization).

Ah, this is why I guess – I was going to propose exactly such a rewrite.

Free regions are always alive, even in hairpin loops

A more “region-inferency” example to the previous one, that shows that we must treat free regions as alive in all cases, and not just at function return points

Yes, I didn’t write up the treatment of free regions yet, but I was roughly thinking of something like this (I’ve been back and forth on the best way…):

• A region if a set of points and/or free regions
• Reworking the analysis to be expressed in terms of “may contain” this point etc, and having regions be considered live on all points, as you say
• As one possible impl strategy, I was contemplating tracking the outlives relationships and saying that when the user writes 'a we will represent that as a set that consists of (a) all the CFG nodes and (b) the 'a node plus © any regions that 'a is declared to outlive. Not sure if that’s a good idea or not, kind of wanted to play around with it.

[nikomatsakis]

A more “region-inferency” example to the previous one, that shows that we must treat free regions as alive in all cases, and not just at function return points (that’s more of an “implementation issue”, but it is something to be aware of).

Hmm, something’s bugging me about this. I think that the “infinite loop” behavior you were talking about is more surprising than I thought at first. Consider this example, where we use a (incorrect, but perhaps unsafe) API to spawn threads, relying on a dtor to join them:

let scope = Scope::new();
let mut foo = 22;

// dtor joins the thread
let _guard = scope.spawn(&mut foo);

loop {
    foo += 1;
}

// drop of `_guard` joins the thread

This code would presumably pass borrowck, since the drop is not reachable, but that seems sort of wrong. Now, of course, this API is not safe: the safe version would use a closure, and then having “special treatment” of free regions like 'a (where it is treated as live throughout the closure body) would make things work, but that feels suboptimal. It’d be nice if we could inline the closure body and preserve the same level of type soundness. =)

I had considered in the past that MIR construction could insert false “break” edges onto infinite loops. This is a common enough technique in compilers, since some algorithms are better behaved if there is a universal path to the exit. This would not completely eliminate dead code – example, code that is dominated by a return or break would still be dead – but it would ensure that the EXIT block is always reachable from the START block, right? Might be something to consider.

[nikomatsakis]

Hmm, something’s bugging me about this.

To narrow down a bit more, it feels like we ought to be able to treat named regions as an extension of the existing control-flow graph, and not have them be a special case.

[nikomatsakis]

I had considered in the past that MIR construction could insert false “break” edges onto infinite loops. This is a common enough technique in compilers, since some algorithms are better behaved if there is a universal path to the exit. This would not completely eliminate dead code – example, code that is dominated by a return or break would still be dead – but it would ensure that the EXIT block is always reachable from the START block, right? Might be something to consider.

I was thinking about this more in the meantime, and I think that – if we were going to go down this path – the right way would be to have loop be considered to have a (false) unwind edge. I believe this would ensure that the CFG has a single exit (well, the union of the RETURN and RESUME exits).

I’m technically on vacation now =), but on the airplane I prototyped out how this would work in the free-regions branch of the nll repository. In that branch, I made, for each free lifetime, synthetic graph nodes that follow from RETURN/RESUME; the free lifetimes are considered live in those nodes. Anyway, the internet here is too slow for me to go into details… (plus: vacation)… will try to post more later. =)

[RalfJung]

This looks great, I am particularly happy to see the error messages work out so nicely. I was worried that could become a major pain with NLL, but this 3-point-patterns is very effective.

I first was somewhat upset by lifetimes having holes, but indeed that is somewhat the case even in problem case #3 so I suppose that’s just necessary. In talking with @nikomatsakis earlier today, one thing that came up is that lifetimes currently have a clear end, but not really a clear start. I like that, it matches what I am doing in my formal model. However, due to the gaps, the lifetimes in this proposal do not really have a clear end any more. I will have to think more about what to make of this.

---

The one item in the proposal which leaves me most uneasy is the part about adding artificial nodes to the CFG to represent named external lifetimes. This thread has already uncovered problems wrt. infinite loops (and the proposed solution of adding an exit edge seems like a hack to me). Also, to represent arbitrary lattices of lifetime inclusions, the artifical blocks may sometimes have multiple successors, making them look even more artificial.

Why did you even choose this interesting approach to handling external lifetimes? I would have expected something based more on the fact that return takes an argument of a particular type, giving rise to appropriate constraints.

TBH I do not see immediately what your example is supposed to demonstrate @arielb1. Which type should send_to_other_thread have?

[nikomatsakis]

This topic was automatically closed 90 days after the last reply. New replies are no longer allowed.