Nice post! I’m trying to work out through it.
It looks like the main idea is that by keeping track of relationships between regions, instead of the exact lifetime of regions, we don’t have to keep track of dead regions, which prevents different “initializations” .
I disagree with this proposal “avoiding SSA”. From my reading of it, it keeps track of a different region graph for every CFG point, which is basically a full CPS transformation, which SSA is supposed to be an optimized version of.
Forgotten lifetiems - region inference as quantifier elimination
I should really finish writing this, but I want to get this post out and I don’t have an infinite amount of time.
If we allow ourselves to take a full “CFG -> CPS transformation”, and do region inference on that, then our code becomes a bunch of lambdas wrapped about a fixed-point combinator:
start/1
x = use() ; -> start/2
start/2
y = use() ; -> start/3
start/3
list = &'b1 mut x ; -> start/4 'list
start/4 'list
v = &'b2 mut (*list).value ; -> start/5 'list 'v
start/5 'list 'v
list = &'b3 mut y ; -> start/6 'list 'v
start/6 'list 'v
use(v) ; -> start/7 'list
start/7 'list
use(list);
In order to borrow-check the program, each CFG pointCPS lambda needs to know the relationship between the regions that enter it, and the loans that it must not modify, and region inference is basically propagating these constraints across the CFG.
Now, the regions that enter each CPS lambda have no direct relationship to the regions that exit it - the only relationship is through the loans and the stack trace. Therefore, if we don’t want, at each CFG point, to keep track of every region from every CFG point - and this is an infinite set of regions if the CFG contains a loop - we need to “forget” lifetimes that are going to be dead.
This “forgetting” of region variables is basically quantifier elimination - the caller knows that the conditions on the “external” regions hold for some set of “internal” regions, and it wants to eliminate the internal regions.
I’ll note that closures perform the same thing where they want to “forget” about a region. In that case, we don’t have a complete solution. This confused at least me - I stopped looking for a solution along these lines for non-closure inference, because I thought it would have to be incomplete.
However, the difference between these cases is:
- In the closure case, we want, for our given
φ representing the conditions on the closure, a ψ such that ψ('lts) ≡ ∀'x φ('x, 'lts), which is not trivial to do in a complete way.
- In the non-closure case, we want, for our given
φ representing the conditions on the “abandonment point”, a ψ such that ψ('lts) ≡ ∃'x φ('x, 'lts). This is equivalent to just “cutting out” 'x from the region graph, and definitely doable.
Now, to see what I mean, let’s see some code:
Loops, play-by-play
So, to give names to the lifetimes in the loop example:
fn main() {
let mut base = &'base mut Thing;
loop {
// no relation between 'base & 't
let t = &'t mut *base; // 'base: 't
let c: Option<&'t mut Thing> = maybe_next({t});
match c {
Some(v) => {
temp = v;
// 't: 'base ('t `includes` 'base)
}
None => {
// 't ends here
}
}
}
}
Here, crucially, this code is sound because a 't region from this iteration of the loop can’t be alive at the None arm - and therefore, the borrow of base can’t go through that arm.
However, a 't region from a previous iteration of this loop can certainly be alive here (e.g. if we go through the Some arm and then the None arm), so some 't region can be alive here. The current NLL code treats all the regions with the same origin as through they are the same region, and therefore ends up with an error.
I think this works:
struct List<+> {
value: 0,
}
let x: List<()>;
let y: List<()>;
let list: &'list mut List<()>;
let v: &'v mut ();
block START {
// ()
x = use();
y = use();
//
list = &'b1 mut x;
// 'v: 'b1, 'b1: 'list
v = &'b2 mut (*list).value;
// 'v: 'b1: 'list: 'b2: 'v
list = &'b3 mut y;
// We forget the old 'list in the assignment
// 'v: 'b1: 'b2: 'v; 'b3: 'list
use(v);
// nothing here keeps 'v alive.
use(list);
}
I think it is really helpful to do away with the outlives terminology. I've always thought it confusing to use terminology that is indicative of 