Stream: t-compiler/wg-nll

Topic: relations-between-regions


Alex Horn (Jun 19 2018 at 03:28, on Zulip):

Hello! I hope this is the right place to ask a question about the "alias-based formulation of the borrow checker" blog post [0]? Specifically, I had a question about the "Relations between regions" section in the blog post.

For example, on line let r: &'1 mut Vec<&'2 i32> = &'3 mut vit is asserted that both '0: '2 and '2: '0 hold. I would have expected the former ('0: 2) to hold, but not necessarily the latter ('2: '0). What happens if another vector is assigned to reference r?

I would greatly appreciate if someone could clarify how these "region" subset facts are computed in general. If possible, I would like to follow the example in detail to the end (e.g., a later argument relies on '4: '5: '2: '0).

Many thanks in advance!

[0] http://smallcultfollowing.com/babysteps/blog/2018/04/27/an-alias-based-formulation-of-the-borrow-checker/

nikomatsakis (Jun 19 2018 at 08:14, on Zulip):

they derive from the subtyping relationships and other parts of the MIR type check; in that particular case, &mut T is invariant with respect to T, so &mut T <: &mut U requires that T = U (and hence that &'2 i32 = &'0 i32 in this particular example). '2 = '0 if '2: '0 and '0: '2

Alex Horn (Jun 19 2018 at 18:55, on Zulip):

Thanks! From an alias analysis perspective, using similar reasoning as above, I find it surprising that '0 = '1 = '3 would hold (rather than merely '0 : '3 and '1: '3) in the following example where u : Vec<&'0 i32> and v : Vec<&'1 i32> are two different vectors:

a. let mut r: &'2 mut Vec<'3 &i32>; b. r = &'4 mut v; c. r = &'5 mut u;

Is there any documentation that I could read to better this case? My confusion may stem from the fact that I think too much about alias analysis rather than type checking. In particular, I am reading subsets such as '4 : '2 and '5 : '2 to be similar to the subsets in Andersen's algorithm.

nikomatsakis (Jun 19 2018 at 19:06, on Zulip):

I don't believe I said that '1 and '3 would be related

nikomatsakis (Jun 19 2018 at 19:07, on Zulip):

I'm not sure if we're talking about precisely the same example :)

Alex Horn (Jun 19 2018 at 21:28, on Zulip):

Sorry, I sought to illustrate the second part of my earlier question, namely: "What happens if another vector is assigned to reference r?"

On the surface, both examples share in common that they require a region 'R as in Vec<'R &i32> to be related to another region:

1\ Specifically, in the first example, reference r is only assigned once (using v) and 'R turns out to be equal to another region.
2\ In the second example, r is assigned twice (using u and v), but your response indicates that no such region _equality_ is induced then.

My goal was to better understand by comparing and contrasting both examples. Any suggestion that may get me back on the right track are welcome! :)

Alex Horn (Jun 19 2018 at 21:33, on Zulip):

Any suggestion that may get me back on the right track are welcome! :)

In other words, eventually if possible, I would like to be able to pick apart both examples by appealing to the right inference rules that are being used to setup the subset region relationships. I know a bit weird maybe, I am just curious.

Vytautas Astrauskas (Jun 20 2018 at 14:13, on Zulip):

@Alex Horn An important point in Polonius is that the relations are per program point. So, in your second example, you will get that the relation '3 = '1 holds on a set of program points, and the relation '3 = '0 holds on some other set of points. Only if these two sets overlap, you will get a relation '1 = '0.

Vytautas Astrauskas (Jun 20 2018 at 14:13, on Zulip):

Does this help?

Alex Horn (Jun 20 2018 at 16:28, on Zulip):

This helps, thank you! What I am still unclear about is: when do sets of program points "overlap"? I understood the cfg_edge(P, Q) fact and has it is used to propagate subset relations. In the second example, cfg_edge(a, b) and cfg_edge(b, c).

Vytautas Astrauskas (Jun 20 2018 at 17:47, on Zulip):

Niko in his blog post does not talk about at which program points a specific relation holds. Instead, he talks about what relations hold at a specific program point, which is basically the same thing just phrased differently. For example, the fact subset(R1, R2, P) expresses that the subset relation between regions R1 and R2 holds at the program point P. Now if you have a set of subset facts, you can compute at which set of program points P the subset relation between R1 and R2 holds.

Vytautas Astrauskas (Jun 20 2018 at 17:50, on Zulip):

To answer your question: a set of program points that expresses the subset relation between R1 and R2 overlap with a set of program points that expresses the relation between R2 and R3 if there exists such a program point P that the facts subset(R1, R2, P) and subset(R2, R3, P) can be derived.

Vytautas Astrauskas (Jun 20 2018 at 17:51, on Zulip):

Is it clearer?

Alex Horn (Jun 20 2018 at 20:50, on Zulip):

Awesome, thanks for taking the time to clarify; I appreciate it!

Let me make sure I understand. Here is a proof of '0 = '1 = '3 for the second example:

As previously discussed, we know that the relation '3 = '0 holds at program point b. Similarly, '3 = '1 at program point c. By definition, cfg_edge(b, c). Hence, by Rule subset3 (version 1), '3 = '0 at program point c. Therefore, since '3 = '0and '3 = '1 at program point c, we conclude '0 = '1 = '3.

I find this equality surprising. Is this result expected?

One of @nikomatsakis 's earlier comments reads: "I don't believe I said that '1 and '3 would be related". I did not fully understand his comment. May I am misinterpreting the later assertion that we "will get that the relation '3 = '1" .

nikomatsakis (Jun 20 2018 at 21:12, on Zulip):

sorry @Alex Horn, I'm multi-plexing a bunch of stuff lately, but I'm finding it hard to understand your examples. =) Probably if I went back up and re-read your examples I would understand better. I would however appreciate copying and pasting all the information together in one place (i.e., not referencing any previous message :) Just looking at what I see in zulip I still don't quite see where '0 = '1 = '3 is coming from etc. (For example, I don't know what program point c or b refers to, etc.)

I would like to see the input program (ideally in MIR-like format, but Rust-like is ok too).

Alex Horn (Jun 21 2018 at 05:19, on Zulip):

Will definitely do, I shall draft something. Thanks.

Alex Horn (Jun 21 2018 at 17:44, on Zulip):

I've created a v0-draft: https://pastebin.com/w53KTyzs.

To keep things simple, the live analysis is assumed to be disabled.

What are the intended relations between the regions here?

If '0 == '1 == '7 holds (which may or may not be the case), what are the implications on the analysis (if any)?

To further guide the discussion, I repeat (at times verbatim) what I understood our discussion to imply about the v0-example:

A\ On line 15 (r = &/* '8 */ mut u), &mut T is invariant with respect toT, so &mut T <: &mut U requires that T = U. Hence, '0 = '7.
B\ Similarly on line 18 (r = &/* '9 */ mut v), '1 = '7.
C\ By definition, cfg_edge(line 17, line 18)(transitively).
D\ Hence, by Rule subset3 (version 1), we get '0 = '7 on line 18.
E\ Therefore, since '0 = '7 and '1 = '7 on line 18, '0 = '1 = '7 holds.

Keith Yeung (Jun 21 2018 at 20:05, on Zulip):

I think we're all confused about this '0 = '1 notation, what is this all about?

Keith Yeung (Jun 21 2018 at 20:05, on Zulip):

do you mean '0: '1 instead?

nikomatsakis (Jun 21 2018 at 20:42, on Zulip):

'0 = '1 I believe means '0: '1 and '1: '0

nikomatsakis (Jun 21 2018 at 20:42, on Zulip):

@Alex Horn I looked at the example and wrote some notes

nikomatsakis (Jun 21 2018 at 20:43, on Zulip):

One part of it is the liveness results — those currently cause the two assignments to r to be distinguished

nikomatsakis (Jun 21 2018 at 20:43, on Zulip):

I think that is an element of the system we might change; but if we did so, then it would yes imply a loss of resolution

nikomatsakis (Jun 21 2018 at 20:44, on Zulip):

is that what you are saying?

Alex Horn (Jun 21 2018 at 21:35, on Zulip):

Read your notes, very enlightening. Yes, I am aiming to better understand the strengths and weaknesses of the proposed approach, which I find very interesting. In addition, I am curious how it relates to previous work, in case they are lessons from the past that could broaden my perspective.

nikomatsakis (Jun 22 2018 at 10:27, on Zulip):

I'd appreciate any insights :)

Last update: Nov 21 2019 at 13:10UTC