Stream: t-compiler/wg-polonius

Topic: placeholder loans vs subsets


lqd (Aug 03 2020 at 14:42, on Zulip):

this is mostly an implementation detail in my mind

nikomatsakis (Aug 03 2020 at 14:42, on Zulip):

I agree but it's worth trying to settle it

nikomatsakis (Aug 03 2020 at 14:42, on Zulip):

I'd also be curious to hear from @Aaron Weiss a bit more about the oxide side of things, but maybe he's not able to communicate much at present

lqd (Aug 03 2020 at 14:43, on Zulip):

oh of course it's worth doing so, I didn't mean to imply the opposite sorry

Aaron Weiss (Aug 03 2020 at 15:00, on Zulip):

So, if I recall correctly, this is ultimately a question of how to address relationships between quantified provenances/lifetimes, right?

Aaron Weiss (Aug 03 2020 at 15:02, on Zulip):

Or well, between the local kind and the quantified kind.

Aaron Weiss (Aug 03 2020 at 15:04, on Zulip):

If so, I think we probably have deviated somewhat from Polonius in this area, but what we do is closer to subsets. In particular, we don’t associate any sets directly with quantified provenances, and we relate local and qualified provenances only when the former’s loan sets consist of reborrows from qualified provenances that outlive the qualified provenance in question.

nikomatsakis (Aug 03 2020 at 15:04, on Zulip):

right

nikomatsakis (Aug 03 2020 at 15:05, on Zulip):

in my original formulation I wrote in this blog post, we basically looked at the set of "required subset relations" between origins/regions and reported errors if those exceeded what the where clause permitted

nikomatsakis (Aug 03 2020 at 15:06, on Zulip):

but then we switched to having "placeholder loans"

nikomatsakis (Aug 03 2020 at 15:06, on Zulip):

it's very, very similar, it's maybe a bit messier, but it has the advantage that you can always replace an origin with a set of loans

nikomatsakis (Aug 03 2020 at 15:06, on Zulip):

I think "provenance = origin"

nikomatsakis (Aug 03 2020 at 15:07, on Zulip):
subset_error(R1, R2, P) :-
  subset(R1, R2, P),      // `R1: R2` required at `P`
  placeholder_region(R1), // `R1` is a placeholder
  placeholder_region(R2), // `R2` is also a placeholder
  !known_subset(R1, R2).  // `R1: R2` is not a "known subset" relation.
nikomatsakis (Aug 03 2020 at 15:07, on Zulip):

that's from the blog post, it was kind of the key rule

nikomatsakis (Aug 03 2020 at 15:07, on Zulip):

I guess I'm open to either formulation, I did like being able to replace origins with "sets of loans" entirely

nikomatsakis (Aug 03 2020 at 15:08, on Zulip):

but I think it's mostly a conceptual thing

nikomatsakis (Aug 03 2020 at 15:08, on Zulip):

still it made it more obviously equivalent to some of the formalisms I've seen proposd

Aaron Weiss (Aug 03 2020 at 15:13, on Zulip):

Yeah, so I think that what we’re doing is more or less looking at the required subset relations. In our setting, it’s a subtyping-style constraint, but checking the relation on a local and qualified provenance has us basically drudge up whatever qualified provenances the local one was reborrowed from (using loans that contain a dereference which I’ve been calling “reborrow loans”) and check that the relation holds from the where bounds.

Aaron Weiss (Aug 03 2020 at 15:14, on Zulip):

I don’t know that we really had a good reason for doing one or the other except that the path through the design space I took ended up with these reborrow loans and this style of solution seemed most apparent to me at the time. Maybe just because of distance from when we discussed placeholders.

Aaron Weiss (Aug 03 2020 at 15:17, on Zulip):

I do think the idea of being able to replace origins with sets of loans is a nice one because it gives a clear sense of what an origin “means.”

nikomatsakis (Aug 03 2020 at 15:20, on Zulip):

Right

nikomatsakis (Aug 03 2020 at 15:20, on Zulip):

That was my main concern, that otherwise it was like "an origin is a set of loans, but also it has an identity of its own"

nikomatsakis (Aug 03 2020 at 15:21, on Zulip):

that said

Aaron Weiss (Aug 03 2020 at 15:21, on Zulip):

Yeah, that’s more-or-less what they are in Oxide right now. The identity matters for at least a few pieces of our system.

nikomatsakis (Aug 03 2020 at 15:21, on Zulip):

origins always have something of a persistent identity

nikomatsakis (Aug 03 2020 at 15:21, on Zulip):

i.e., in today's formulation, we track the subsets which must hold between origins -- and those "flow forward" and must be maintained in later bits of the CFG

nikomatsakis (Aug 03 2020 at 15:21, on Zulip):

in the equality variant, the same is true, but just less commonly

nikomatsakis (Aug 03 2020 at 15:22, on Zulip):

so it's not like you could ever truly erase the origins I guess

Aaron Weiss (Aug 03 2020 at 15:22, on Zulip):

In the sense that you need to know which ones flow forward and which ones don’t?

nikomatsakis (Aug 03 2020 at 15:22, on Zulip):

my memory of oxide is dated

nikomatsakis (Aug 03 2020 at 15:22, on Zulip):

but what I remember from there was that

nikomatsakis (Aug 03 2020 at 15:23, on Zulip):

in invariant contexts, you would have to have the same origin in the type

nikomatsakis (Aug 03 2020 at 15:23, on Zulip):

Aaron Weiss said:

In the sense that you need to know which ones flow forward and which ones don’t?

right in the sense that you have to remember which origins must remain equal to one another because they got "entangled" b some previous bit of code

nikomatsakis (Aug 03 2020 at 15:24, on Zulip):

this is basically our way of encoding the flow-sensitive type system..

nikomatsakis (Aug 03 2020 at 15:24, on Zulip):

examples and some related discussion

nikomatsakis (Aug 03 2020 at 15:24, on Zulip):

this is the key example

let v: Vec<&'v u32> = vec![];
let p: &mut Vec<&'p u32> = &mut v;
p.push(...); // any changes to 'p here *should* affect 'v
nikomatsakis (Aug 03 2020 at 15:24, on Zulip):

here, 'v and 'p are not independent

nikomatsakis (Aug 03 2020 at 15:24, on Zulip):

my recollection is that oxide would've required that the user write 'v in p

Aaron Weiss (Aug 03 2020 at 15:25, on Zulip):

re: invariant contexts, If that wasn’t true in the past, it’s true now because we actually have an ordering on our environments and we require provenances to occur earlier in the environment in order to outlive another. So, invariance would require that to be true in both directions meaning it would have to be exactly the same.

nikomatsakis (Aug 03 2020 at 15:25, on Zulip):

(and indeed we formulated a variant like that, but then found that it was too flow insensitive to accept this example)

Aaron Weiss (Aug 03 2020 at 15:28, on Zulip):

So, what you’re doing is essentially allowing them the different names, but recording that ‘v and ‘p are equal?

nikomatsakis (Aug 03 2020 at 15:29, on Zulip):

correct

nikomatsakis (Aug 03 2020 at 15:30, on Zulip):

the interesting part about that is that this equality can be flow-sensitive

nikomatsakis (Aug 03 2020 at 15:30, on Zulip):

(the same is true in our code today, except that we are not recording equality but p <= q relations)

Aaron Weiss (Aug 03 2020 at 15:34, on Zulip):

I think Oxide in its current form would reject the example you just linked for essentially the same reason the flow-insensitive equality would.

Aaron Weiss (Aug 03 2020 at 15:37, on Zulip):

The fact that the identity of origins does matter then makes the argument for placeholder loans less compelling to me personally.

Aaron Weiss (Aug 03 2020 at 15:38, on Zulip):

Since it does really mean that an origin is always a set of loans with a unique identity plus context-dependent constraints on the relationship between those identities.

lqd (Aug 03 2020 at 15:41, on Zulip):

(I myself was mostly assuming the theoretical aspect would be relatively similar between the 2 but didn't think about the impact on the Equality variant or invariance; on the operational side, placeholder loans mesh well with location insensitivity, but not with trying to limit the propagation of subsets; I like the neatness of the model using placeholder loans, and origins as set of loans, but at the same time I see loan propagation as just materializing the fact that two origins were once reachable via space/subsets and time/cfg -- and hoped we could sometimes avoid materializing them altogether)

nikomatsakis (Aug 03 2020 at 16:09, on Zulip):

ack, I think I have the other topics in this stream not visible

nikomatsakis (Aug 03 2020 at 16:10, on Zulip):

so I think I persuaded myself that we don't need to do everything via placeholders

nikomatsakis (Aug 03 2020 at 16:10, on Zulip):

for the reason that we still can't just replace origins with sets of loans

nikomatsakis (Aug 03 2020 at 16:11, on Zulip):

so really you can't think of the polonius rules that way, or at least, it's a non-trivial change to achieve it

nikomatsakis (Aug 03 2020 at 16:16, on Zulip):

should we @lqd adjust the hackmd rules to match and try to make polonius match then?

lqd (Aug 03 2020 at 16:18, on Zulip):

modify the rules to compute subset errors via rules about subsets ?

nikomatsakis (Aug 03 2020 at 16:21, on Zulip):

yeah I mean it's a pretty small modification I guess

lqd (Aug 03 2020 at 16:21, on Zulip):

I'll start gathering those

lqd (Aug 03 2020 at 16:21, on Zulip):

I'll do it

lqd (Aug 03 2020 at 16:22, on Zulip):

so you can focus on more important things

lqd (Aug 03 2020 at 16:24, on Zulip):

I guess I could also add the location-insensitive rules to the hackmd at the same time (as it can still use placeholder loans very naturally anyways)

nikomatsakis (Aug 03 2020 at 16:28, on Zulip):

which rules do you mean?

nikomatsakis (Aug 03 2020 at 16:28, on Zulip):

but that sounds useful

lqd (Aug 03 2020 at 16:29, on Zulip):

the simple rules used by the location-insensitive analysis

nikomatsakis (Aug 03 2020 at 16:30, on Zulip):

how do they rely on placeholder loans?

lqd (Aug 03 2020 at 16:30, on Zulip):

they don't yet, but in order to still have a fast pre-pass we can "potential subset errors" to the location-insensitive analysis

lqd (Aug 03 2020 at 16:33, on Zulip):

(it probably wouldn't be complicated to add the subset-errors via subset rules, but for placeholder loans I think it was literally a single character change)

nikomatsakis (Aug 03 2020 at 16:33, on Zulip):

right, so, the location insensitive analysis computes SUBSET(OriginA, OriginB) across the whole CFG, right?

nikomatsakis (Aug 03 2020 at 16:34, on Zulip):

so presumably we could determine whether any placeholders wind up that set?

nikomatsakis (Aug 03 2020 at 16:34, on Zulip):

er, I mean, whether any "placeholder origins" wind up in that set

nikomatsakis (Aug 03 2020 at 16:34, on Zulip):

I guess it's not clear how that would help us maybe

lqd (Aug 03 2020 at 16:37, on Zulip):

yes that's what the the analysis does and indeed just checking whether a placeholder loan ends up in there was easy

nikomatsakis (Aug 03 2020 at 16:39, on Zulip):

I guess though that if we adopt the "subset relation" approach to reporting errors, well, I suppose it can still be useful

nikomatsakis (Aug 03 2020 at 16:39, on Zulip):

I was thinking that it wouldn't obviously help in allowing us to avoid computation but

lqd (Aug 03 2020 at 16:39, on Zulip):

it doesn't help us that much more than the regular subset-rules subset errors but it mapped naturally to this existing relation, compared to having more relations; it was mostly cute that a single character was enough to make the placeholder loan computation location-insensitive

nikomatsakis (Aug 03 2020 at 16:39, on Zulip):

at least the subset_error can only iterate over placeholder origins that may be involved in errors

lqd (Aug 03 2020 at 16:40, on Zulip):

(also the outlives_everywhere idea to fix the OOM mapped naturally to the location-insensitive analysis)

lqd (Aug 03 2020 at 16:41, on Zulip):

my recollection is that these potential loan errors and potential subset errors do allow for a lot of filtering in the regular location-sensitive analyses

nikomatsakis (Aug 03 2020 at 17:17, on Zulip):

the real win would be if we can compute fewer subset relations

nikomatsakis (Aug 03 2020 at 17:17, on Zulip):

(at least in this specific case)

lqd (Aug 03 2020 at 18:18, on Zulip):

that's also interesting as splitting subset errors from placeholder loans can allow to filter the data independently with the results of the pre-pass

lqd (Aug 03 2020 at 18:22, on Zulip):

I recall that when we heavily filtered the outlives relation to remove all the subsets which couldn't easily reach an error, it had quite an impact on clap, and that's the kind of things we can't easily do when both are intertwined

Last update: Jun 20 2021 at 00:45UTC