## 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 ? 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 v`it 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).

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 = '0`and `'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 to`T`, 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: Jul 02 2020 at 12:20UTC