An alias-based formulation of the borrow checker (2018)

Ever since the Rust All Hands, I’ve been experimenting with an alternative formulation of the Rust borrow checker. The goal is to find a formulation that overcomes some shortcomings of the current proposal while hopefully also being faster to compute. I have implemented a prototype for this analysis. It passes the full NLL test suite and also handles a few cases – such as #47680 – that the current NLL analysis cannot handle. However, the performance has a long way to go (it is currently slower than existing analysis). That said, I haven’t even begun to optimize yet, and I know I am doing some naive and inefficient things that can definitely be done better; so I am still optimistic we’ll be able to make big strides there.

Also, it was pointed out to me that yesterday, April 26, is the sixth “birthday” of the borrow check – it’s fun to look at my commit from that time, gives a good picture of what Rust was like then.

End-users don’t have to care

The first thing to note is that this proposal makes no difference from the point of view of an end-user of Rust. That is, the borrow checker ought to work the same as it would have under the NLL proposal, more or less.

However, there are some subtle shifts in this proposal in terms of how the compiler thinks about your program, and that could potentially affect future language features.

Our first example

The analysis works on MIR, but I’m going to explain it in terms of simple Rust examples. Here is the first example, which I will call example A. The example should not compile, as you can see:

fn main () { let mut x : i32 = 22 ; let mut v : Vec <& i32 > = vec! []; let r : & mut Vec <& i32 > = & mut v ; let p : & i32 = & x ; // 1. `x` is borrowed here to create `p` r . push ( p ); // 2. `p` is stored into `v`, but through `r` x += 1 ; // <-- Error! can't mutate `x` while borrowed take ( v ); // 3. the reference to `x` is later used here } fn take < T > ( p : T ) { .. }

Regions are sets of loans

The biggest shift in this new approach is that when you have a type like &'a i32 , the meaning of 'a changes:

... continue reading