How to reason formally about programs using non lexical lifetimes

user_1272610 0
Viewed 209

Consider the following rust program:

fn main()
{
    let mut x = 1;
    let mut r = &x;
    r;
    let y = 1;
    r = &y;
    x = 2;
    r;
}

It compiles without any errors and I agree with that behaviour.

The problem is that I am not able to reach the same conclusion when trying to reason about this formally:

  1. The type of the variable r is &'a i32 for some lifetime 'a.
  2. The type of &x is &'b i32 for some lifetime 'b.
  3. The lifetime 'a includes x = 2;.
  4. From let mut r = &x; we know that 'b: 'a.
  5. Because of 3 and 4 we know that the lifetime 'b includes x = 2;.
  6. Because of 2 and 5 we are doing x = 2; while borrowing x, so the program should be invalid.

What is wrong with the formal reasoning above, and how would the correct reasoning be?

borrow-checker rust
2 Answers

The lifetime 'a includes x = 2;.

Because of 3 and 4 we know that the lifetime 'b includes x = 2;.

They don't. r is reassigned to on line 7, this ends the entire thing as r is thereafter a completely new value independent from the old one -- and yes rustc is smart enough to work at that granularity, that's why if you remove the final x; it will warn that

value assigned to r is never read

at line 7 (whereas you would not get that warning with Go for instance, the compiler doesn't work at that low a granularity).

Rustc can thus infer that the smallest necessary length for 'b stops somewhere between the end of line 5 and the start of line 7.

Since x doesn't need to be updated before line 8, there is no conflict.

If you remove the assignment, however, 'b now has to extend to the last last line of the enclosing function, triggering a conflict.

Your reasoning seems to be that of lexical lifetimes, rather than NLL. You may want to go through the RFC 2094, it is very detailed. But in essence it works in terms of liveness constraints of values, and solving those constraints. In fact the RFC introduces liveness with an example which is a somewhat more complicated version of your situation:

let mut foo: T = ...;
let mut bar: T = ...;
let mut p: &'p T = &foo;
// `p` is live here: its value may be used on the next line.
if condition {
    // `p` is live here: its value will be used on the next line.
    print(*p);
    // `p` is DEAD here: its value will not be used.
    p = &bar;
    // `p` is live here: its value will be used later.
}
// `p` is live here: its value may be used on the next line.
print(*p);
// `p` is DEAD here: its value will not be used.

Also note this quote which very much applies to your misunderstanding:

The key point is that p becomes dead (not live) in the span before it is reassigned. This is true even though the variable p will be used again, because the value that is in p will not be used.

So you really need to reason off of values, not variables. Using SSA in your head probably helps there.

Applying this to your version:

let mut x = 1;
let mut r = &x;
// `r` is live here: its value will be used on the next line
r;
// `r` is DEAD here: its value will never be used
let y = 1;
r = &y;
// `r` is live here: its value will be used later
x = 2;
r;
// `r` is DEAD here: the scope ends
user_81821180

Life before NLL

Before discussing about non-lexical lifetimes (NLL), let's first discuss the "ordinary" lifetimes. In older Rust before NLL is introduced, the code below won't compile because r is still in scope while x is mutated in row 3.

let mut x = 1;
let mut r = &x;
x = 2; // Compile error

To fix this, we need to explicitly make r out of scope before x is mutated:

let mut x = 1;
{
    let mut r = &x;
}
x = 2;

At this point you might think: If after the line of x = 2, r is not used anymore, the first snippet should be safe. Can the compiler be smarter so that we don't need to explicitly make r out of scope like we did in the second snippet?

The answer is yes, and that's when NLL comes in.

Life after NLL

After NLL is introduced in Rust, our life becomes easier. The code below will compile:

let mut x = 1;
let mut r = &x;
x = 2; // Compiles under NLL

But remember, it will compile as long as r is not used after the mutation of x. For example, this won't compile even under NLL:

let mut x = 1;
let mut r = &x;
x = 2; // Compile error: cannot assign to `x` because it is borrowed
r;     //                borrow later used here

Although the rules of NLL described in RFC 2094 are quite complex, they can be summarized roughly and approximately (in most cases) as:

A program is valid as long as every owned value is not mutated between the assignment of a variable referring to it and the usage of that variable.

The code below is valid because x is mutated before the assignment of r and before the usage of r:

let mut x = 1;
x = 2;          // x is mutated
let mut r = &x; // r is assigned here
r;              // r is used here

The code below is valid because x is mutated after the assignment of r and after the usage of r:

let mut x = 1;
let mut r = &x; // r is assigned here
r;              // r is used here
x = 2;          // x is mutated

The code below is NOT valid because x is mutated after the assignment of r and before the usage of r:

let mut x = 1;
let mut r = &x; // r is assigned here
x = 2;          // x is mutated
r;              // r is used here      -> compile error

To your specific program, it's valid because when x is mutated (x = 2), there is no variable referring to x anymore—r is now referring to y because of the previous line (r = &y). Therefore, the rule is still adhered.

let mut x = 1;
let mut r = &x;
r;
let y = 1;

r = &y;

// This mutation of x is seemingly sandwiched between
// the assignment of r above and the usage of r below,
// but it's okay as r is now referring to y and not x
x = 2;

r;
user_14035300
Related