Stream: t-compiler/wg-nll

Topic: subset-outlives-what-fun


nikomatsakis (May 11 2018 at 13:50, on Zulip):

@Santiago Pastorino ok so —

nikomatsakis (May 11 2018 at 13:50, on Zulip):

regarding the origin of those rules in the blog post

nikomatsakis (May 11 2018 at 13:50, on Zulip):

I guess the question was: if we have R1: R2, why do that translate to R1 <= R2 and not R2 <= R1?

nikomatsakis (May 11 2018 at 13:50, on Zulip):

in terms of sets of loans?

nikomatsakis (May 11 2018 at 13:51, on Zulip):

and in particular how should we think about that with "outlives"?

nikomatsakis (May 11 2018 at 13:51, on Zulip):

first off, what I personally find useful is to read R1: R2 as "data with region R1 flows into region R2"

nikomatsakis (May 11 2018 at 13:52, on Zulip):

so e.g. if you have

let x: &'0 i32 = ...
let y: &'1 i32 = x;

then this results in '0: '1, because data with region '0 was stored into y, which has region '1

nikomatsakis (May 11 2018 at 13:52, on Zulip):

but outlives is of course also a reasonable way to think of it: in that case, the idea is that the "source" of the data must outlive the target

nikomatsakis (May 11 2018 at 13:53, on Zulip):

anyway, now back to loans: the idea is that each region can be mapped to a set of loans {L} which may be the source of the referenced data

nikomatsakis (May 11 2018 at 13:53, on Zulip):

that is, if you have &'0 u32, and '0 maps to {L1, L2}, then we know that that reference may have been created by the loan L1 or L2, and hence if we invalidate the terms of either loan (e.g., by mutating or accessing the path that was borrowed), then we can't use the reference anymore

nikomatsakis (May 11 2018 at 13:54, on Zulip):

anyway so if you think about it as data flow, then perhaps the <= makes sense: that is, in our example, y was assigned from x (and maybe from other things), so it points to anything that x can point at (and maybe other things)

nikomatsakis (May 11 2018 at 13:55, on Zulip):

if we think about it in terms of "outlives", the key point is that references "live longer" by having fewer loans

nikomatsakis (May 11 2018 at 13:55, on Zulip):

because there are fewer ways to invalidate them

nikomatsakis (May 11 2018 at 13:55, on Zulip):

so since '0 outlives '1, it must be smaller than '1 ("contain" fewer loans)

nikomatsakis (May 11 2018 at 13:56, on Zulip):

@Santiago Pastorino does that explain it?

lqd (May 11 2018 at 14:01, on Zulip):

I was also confused by this :) (possibly because I once thought they were sets of _points_ not of loans; more points being the subset was confusing)" — it's clear now

Santiago Pastorino (May 11 2018 at 14:10, on Zulip):

anyway, now back to loans: the idea is that each region can be mapped to a set of loans {L} which may be the source of the referenced data

remember me about this, I may be confusing again some concepts, a regions maps to a set of loans, explain a bit more :)

Santiago Pastorino (May 11 2018 at 14:12, on Zulip):

a Loan have one region but a region can have more than one Loan

Santiago Pastorino (May 11 2018 at 14:12, on Zulip):

@nikomatsakis was that what you meant?

nikomatsakis (May 11 2018 at 14:12, on Zulip):

loans don't have regions; regions map to a set of loans, however, that they depend on (meaning: for the reference to remain valid, the terms of the loan must be respected)

nikomatsakis (May 11 2018 at 14:13, on Zulip):

I guess you could say a loan has a region in the form of the borrow_region predicate

nikomatsakis (May 11 2018 at 14:13, on Zulip):

in which case what you wrote seems right

nikomatsakis (May 11 2018 at 14:13, on Zulip):

(hmm, I may have called borrow_region something else in the blog post, I can't remember)

Santiago Pastorino (May 11 2018 at 14:14, on Zulip):

it's borrow_region

nikomatsakis (May 11 2018 at 14:14, on Zulip):

point is, when you have a &'a foo expression, that produces a loan L, and {L} <= 'a

nikomatsakis (May 11 2018 at 14:14, on Zulip):

so there is some relationship between L and 'a

nikomatsakis (May 11 2018 at 14:14, on Zulip):

that is, some mapping from L to the region 'a (but 'a may map to many loans)

Santiago Pastorino (May 11 2018 at 14:14, on Zulip):

yep

lqd (May 11 2018 at 14:15, on Zulip):

it's probably just outlivesnamed differently (base_subset)

Santiago Pastorino (May 11 2018 at 14:18, on Zulip):

if we think about it in terms of "outlives", the key point is that references "live longer" by having fewer loans
because there are fewer ways to invalidate them
so since '0 outlives '1, it must be smaller than '1 ("contain" fewer loans)

I understand all this, but dunno how to explain, feels weird :P

Santiago Pastorino (May 11 2018 at 14:19, on Zulip):

seems to me that is defined to be a subset because probabilistically it could live longer?

nikomatsakis (May 11 2018 at 14:19, on Zulip):

(so does it make sense now?) =)

nikomatsakis (May 11 2018 at 14:19, on Zulip):

well anyway feel free to ask more questions if not..

Santiago Pastorino (May 11 2018 at 14:19, on Zulip):

there are fewer ways to invalidate but that doesn't mean it will be invalidated

Santiago Pastorino (May 11 2018 at 14:20, on Zulip):

it's kind of I follow but it doesn't click properly

Santiago Pastorino (May 11 2018 at 14:20, on Zulip):

if you define smaller because it have fewer loans I follow

Santiago Pastorino (May 11 2018 at 14:21, on Zulip):

but in that phrase it confuses me that you used a notion of probability of things to define something

Santiago Pastorino (May 11 2018 at 14:21, on Zulip):

and I find that a bit odd

nikomatsakis (May 11 2018 at 14:22, on Zulip):

but in that phrase it confuses me that you used a notion of probability of things to define something

probability?

nikomatsakis (May 11 2018 at 14:23, on Zulip):

there are fewer ways to invalidate but that doesn't mean it will be invalidated

indeed, the compiler is always conservative in these respects -- i.e., if something bad could happen, it assumes it will happen

nikomatsakis (May 11 2018 at 14:23, on Zulip):

if that is a problem then you have to refine the analysis so that it can see that it will not happen

nikomatsakis (May 11 2018 at 14:24, on Zulip):

which is basically what we are trying to do by moving to NLL :) (that is, we are refining the existing analysis to be more precise)

Santiago Pastorino (May 11 2018 at 14:30, on Zulip):

:+1:

Santiago Pastorino (May 11 2018 at 14:30, on Zulip):

so the definition of subset is because it have fewer loans, right?

Santiago Pastorino (May 11 2018 at 14:31, on Zulip):

if it's that I understood and previously I may have understood some parts of your english in a wrong way :P

Santiago Pastorino (May 11 2018 at 14:31, on Zulip):

it's always hard to follow ;)

nikomatsakis (May 11 2018 at 14:43, on Zulip):

Sounds right

nikomatsakis (May 11 2018 at 18:37, on Zulip):

ok @Santiago Pastorino was asking me about the "dumped tuples"

nikomatsakis (May 11 2018 at 18:37, on Zulip):

and what that's all about

nikomatsakis (May 11 2018 at 18:38, on Zulip):

in the blog post, I talked about these "base inputs"

nikomatsakis (May 11 2018 at 18:38, on Zulip):

e.g., cfg_edge

nikomatsakis (May 11 2018 at 18:38, on Zulip):

right now the compiler has been instrumented to dump out these tuples if you pass -Znll-facts

nikomatsakis (May 11 2018 at 18:38, on Zulip):

they are the starting points for the analysis

nikomatsakis (May 11 2018 at 18:39, on Zulip):

actually @Santiago Pastorino I'm not quite sure what you wanted to know

nikomatsakis (May 11 2018 at 18:39, on Zulip):

:P

nikomatsakis (May 11 2018 at 18:40, on Zulip):

but you can see an example here, in the borrow-check repo

nikomatsakis (May 11 2018 at 18:41, on Zulip):

this is the input rust file -- it's just there for reference, the borrow-check program itself never looks at it

nikomatsakis (May 11 2018 at 18:42, on Zulip):

for each function in the program, we create a directory

nikomatsakis (May 11 2018 at 18:42, on Zulip):

in there are several files

nikomatsakis (May 11 2018 at 18:42, on Zulip):

e.g. cfg_edge.facts

nikomatsakis (May 11 2018 at 18:42, on Zulip):

each line is a tuple, and the individual fields of the tuple are tab-separated

Santiago Pastorino (May 11 2018 at 19:19, on Zulip):

hey, sorry for the delay

Santiago Pastorino (May 11 2018 at 19:20, on Zulip):

yes, makes perfect sense

Santiago Pastorino (May 11 2018 at 19:20, on Zulip):

and sorry to the rest of the people here, I've just read Niko's blog, so still catching up :)

Last update: Nov 21 2019 at 23:25UTC