this is mostly an implementation detail in my mind
I agree but it's worth trying to settle it
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
oh of course it's worth doing so, I didn't mean to imply the opposite sorry
So, if I recall correctly, this is ultimately a question of how to address relationships between quantified provenances/lifetimes, right?
Or well, between the local kind and the quantified kind.
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.
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
but then we switched to having "placeholder loans"
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
I think "provenance = origin"
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.
that's from the blog post, it was kind of the key rule
I guess I'm open to either formulation, I did like being able to replace origins with "sets of loans" entirely
but I think it's mostly a conceptual thing
still it made it more obviously equivalent to some of the formalisms I've seen proposd
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.
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.
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.”
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"
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.
origins always have something of a persistent identity
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
in the equality variant, the same is true, but just less commonly
so it's not like you could ever truly erase the origins I guess
In the sense that you need to know which ones flow forward and which ones don’t?
my memory of oxide is dated
but what I remember from there was that
in invariant contexts, you would have to have the same origin in the type
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
this is basically our way of encoding the flow-sensitive type system..
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
'p are not independent
my recollection is that oxide would've required that the user write
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.
(and indeed we formulated a variant like that, but then found that it was too flow insensitive to accept this example)
So, what you’re doing is essentially allowing them the different names, but recording that ‘v and ‘p are equal?
the interesting part about that is that this equality can be flow-sensitive
(the same is true in our code today, except that we are not recording equality but
p <= q relations)
I think Oxide in its current form would reject the example you just linked for essentially the same reason the flow-insensitive equality would.
The fact that the identity of origins does matter then makes the argument for placeholder loans less compelling to me personally.
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.
(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)
ack, I think I have the other topics in this stream not visible
so I think I persuaded myself that we don't need to do everything via placeholders
for the reason that we still can't just replace origins with sets of loans
so really you can't think of the polonius rules that way, or at least, it's a non-trivial change to achieve it
should we @lqd adjust the hackmd rules to match and try to make polonius match then?
modify the rules to compute subset errors via rules about subsets ?
yeah I mean it's a pretty small modification I guess
I'll start gathering those
I'll do it
so you can focus on more important things
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)
which rules do you mean?
but that sounds useful
the simple rules used by the location-insensitive analysis
how do they rely on placeholder loans?
they don't yet, but in order to still have a fast pre-pass we can "potential subset errors" to the location-insensitive analysis
(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)
right, so, the location insensitive analysis computes
SUBSET(OriginA, OriginB) across the whole CFG, right?
so presumably we could determine whether any placeholders wind up that set?
er, I mean, whether any "placeholder origins" wind up in that set
I guess it's not clear how that would help us maybe
yes that's what the the analysis does and indeed just checking whether a placeholder loan ends up in there was easy
I guess though that if we adopt the "subset relation" approach to reporting errors, well, I suppose it can still be useful
I was thinking that it wouldn't obviously help in allowing us to avoid computation but
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
at least the
subset_error can only iterate over placeholder origins that may be involved in errors
outlives_everywhere idea to fix the OOM mapped naturally to the location-insensitive analysis)
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
the real win would be if we can compute fewer subset relations
(at least in this specific case)
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
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