Stream: t-compiler/wg-polonius

Topic: equality regions


nikomatsakis (Sep 13 2019 at 19:54, on Zulip):

Hey @lqd -- where did you to do your experimentation with adding the "equality" stuff vs propagating all subsets?

lqd (Sep 13 2019 at 19:55, on Zulip):

let me get you the link

lqd (Sep 13 2019 at 19:56, on Zulip):

it's in an old-ish branch, before liveness was integrated, here

lqd (Sep 13 2019 at 19:57, on Zulip):

there were notes I had when we had the video call but I can't quite remember if they reflect the exact state of the branch

lqd (Sep 13 2019 at 19:58, on Zulip):

which is: very hacky, some things were not working so I switched temporarily from doing some computations in datalog in rust just to eliminate a possible source of errors and have flexbility on how to compute equality / propagate it

lqd (Sep 13 2019 at 19:59, on Zulip):

the propagation is likely wrong, as I didn't do a lot of experimentation / or ... thinking (and tests seemed to work)

nikomatsakis (Sep 13 2019 at 20:05, on Zulip):

ok

nikomatsakis (Sep 13 2019 at 20:05, on Zulip):

thanks!

lqd (Sep 13 2019 at 20:07, on Zulip):

yw !

lqd (Sep 13 2019 at 20:08, on Zulip):

(I didn't yet work through the other filtering of interesting regions/provenances I had done on the Naive variant which made it very fast, on this variant)

nikomatsakis (Sep 13 2019 at 20:44, on Zulip):

ok so @lqd I'm looking a bit at the code

nikomatsakis (Sep 13 2019 at 20:45, on Zulip):

I remember that it was quite a bit slower but I don't recall how much we figured out about that

lqd (Sep 13 2019 at 20:45, on Zulip):

the code is called lqd's monster

lqd (Sep 13 2019 at 20:45, on Zulip):

it was slower in that it calculated a lot more subsets IIRC

nikomatsakis (Sep 13 2019 at 20:45, on Zulip):

because of the transitive subset computation?

lqd (Sep 13 2019 at 20:45, on Zulip):

then I added some early small-ish filtering, and it made fast again on clap

lqd (Sep 13 2019 at 20:45, on Zulip):

yeah IIRC

lqd (Sep 13 2019 at 20:46, on Zulip):

removing uninteresting loans helped the most / a lot IIRC

nikomatsakis (Sep 13 2019 at 20:47, on Zulip):

yeah, that's probably something we should do anyway, though I imagine we might do it in polonius

lqd (Sep 13 2019 at 20:47, on Zulip):

yeah esp in the Hybrid variant

nikomatsakis (Sep 13 2019 at 20:47, on Zulip):

one thing that seems also true is that we could compute the equality(N1, N2) only if N1 < N2, but that might be more annoying than it's worth

lqd (Sep 13 2019 at 20:48, on Zulip):

but generally his theavy filtering (I have another filtering optimization elsewhere which removes most of the TC, it's only doing the TC on subset containing loans which were invalidated) helps a lot, so mch that I wondered if we still needed the Optimized variant

lqd (Sep 13 2019 at 20:49, on Zulip):

but then that impacts the illegal subset relation errors

nikomatsakis (Sep 13 2019 at 20:49, on Zulip):

by "heavy filtering", you are referring to the "non-interesting loans"?

nikomatsakis (Sep 13 2019 at 20:50, on Zulip):

I guess there's really nothing wrong with the filtering

nikomatsakis (Sep 13 2019 at 20:50, on Zulip):

well, it depends on which one we mean, but e.g. the rules to remove (R, R) subset relations seem "ok"

lqd (Sep 13 2019 at 20:50, on Zulip):

these loans yes, but also limiting to "interesting regions"

lqd (Sep 13 2019 at 20:51, on Zulip):

(I'll get you a link to the code that will be clearer I think)

nikomatsakis (Sep 13 2019 at 20:51, on Zulip):

OK. I'm going to have to go in a bit, got a call

lqd (Sep 13 2019 at 20:52, on Zulip):

here it is

lqd (Sep 13 2019 at 20:53, on Zulip):

and of course the requires.insert(interesting_borrow_region);

nikomatsakis (Sep 13 2019 at 20:55, on Zulip):

ah

lqd (Sep 13 2019 at 20:55, on Zulip):

it helps a lot on clap but probably it's not the worst use-case, the ongoing benchmarking will clear that up; at least rustc tests pass with it, a bit reassuring but we'll see :)

nikomatsakis (Sep 13 2019 at 20:55, on Zulip):

yeah

nikomatsakis (Sep 13 2019 at 20:55, on Zulip):

that's nice, though

nikomatsakis (Sep 13 2019 at 20:55, on Zulip):

we do a similar opt in NLL but I like how this kind of "flows out" from the invalidation facts

lqd (Sep 13 2019 at 20:56, on Zulip):

it's really just filtering before doing the joins

lqd (Sep 13 2019 at 20:56, on Zulip):

instead of after

nikomatsakis (Sep 13 2019 at 20:56, on Zulip):

right

nikomatsakis (Sep 13 2019 at 20:56, on Zulip):

well i'd be happy if we can wind up with something closer to the naive rules ;)

lqd (Sep 13 2019 at 20:56, on Zulip):

but ofc "illegal subset relation errors" might need the intermediate computations :/

lqd (Sep 13 2019 at 20:56, on Zulip):

haha yeah me too :)

lqd (Sep 13 2019 at 20:57, on Zulip):

it seemed faster than the location_insensitive variant on clap

nikomatsakis (Sep 13 2019 at 20:57, on Zulip):

I remember thinking that this was part of the promise of equality tracking though

nikomatsakis (Sep 13 2019 at 20:57, on Zulip):

ofc this could be combined with location-insensitive, too

lqd (Sep 13 2019 at 20:57, on Zulip):

yes I ahve it elsewhere as well

nikomatsakis (Sep 13 2019 at 20:58, on Zulip):

I'm torn; I'm feeling some sort of desire to delete all the "semi-optimized variants" and get back to naive though

lqd (Sep 13 2019 at 20:58, on Zulip):

part of it yes was in the equality-tracking variant, in total I think 2-3 relations were filtered, this one has all the filters, the eq-tracking one only 1 I think

nikomatsakis (Sep 13 2019 at 20:58, on Zulip):

e.g., delete datafrog-opt, hybrid, location-insensitive, clean up the naive to work just how we want it, and then try to optimize again

nikomatsakis (Sep 13 2019 at 20:58, on Zulip):

but man that can be awfully slow :P

lqd (Sep 13 2019 at 20:58, on Zulip):

:)

nikomatsakis (Sep 13 2019 at 20:58, on Zulip):

but if we can do some judicious filtering like that, it might work

lqd (Sep 13 2019 at 20:59, on Zulip):

we could do that, but maybe just wait until we have the illegal subsets a bit more planned out

lqd (Sep 13 2019 at 20:59, on Zulip):

esp I wondered about the placeholder loans and what will that end up needing wrt intermediate computations of subsets and all

nikomatsakis (Sep 13 2019 at 21:00, on Zulip):

yeah ok next time I carve out some time I'll try to mock up what that means

nikomatsakis (Sep 13 2019 at 21:00, on Zulip):

I feel pretty sure we want placeholder loans tho

lqd (Sep 13 2019 at 21:00, on Zulip):

seems likely indeed

nikomatsakis (Sep 13 2019 at 21:00, on Zulip):

I think we want to be able to say that the polonius loop "computes" the set of loans represented by each origin at each point

nikomatsakis (Sep 13 2019 at 21:00, on Zulip):

vs also computing this auxiliary subset thing

nikomatsakis (Sep 13 2019 at 21:00, on Zulip):

I can't remember if there was another reason more than just "it feels better", maybe connected to this equality stuff? anyway gotta go

lqd (Sep 13 2019 at 21:00, on Zulip):

it seems sensible

nikomatsakis (Sep 13 2019 at 21:01, on Zulip):

if nothing else though it maps to oxide better :)

nikomatsakis (Sep 13 2019 at 21:01, on Zulip):

which feels like a good reason

lqd (Sep 13 2019 at 21:01, on Zulip):

alright cheers niko, enjoy the weekend :)

lqd (Sep 13 2019 at 21:01, on Zulip):

oh yeah for sure

lqd (Sep 13 2019 at 21:13, on Zulip):

(for anyone following at home, the naive rules kinda do 2 TCs, and then filter on static inputs; this filtering is about limiting the amount of work done in the 2 TCs by filtering with these static inputs before the TC, instead of after)

lqd (Sep 20 2019 at 17:17, on Zulip):

I cleaned up the equality prototype a bit, as it used to rely on features of my datafrog fork, and rebased over master

lqd (Sep 20 2019 at 17:17, on Zulip):

the branch is at https://github.com/lqd/borrow-check/tree/variant_prototype2

lqd (Sep 20 2019 at 17:18, on Zulip):

this time it has both versions, with a bool you can toggle in the prototype variant to choose between the 2, and includes the subset/requires filtering, otherwise rustc tests were too slow, and a new input set for all the test cases we mentioned along the way (the "polonius-imprecision" dataset)

lqd (Sep 20 2019 at 17:18, on Zulip):

version 1, implemented from Niko's 1st comment (with itself containing a known imprecision fixed by Niko's 2nd comment): "static equality". TLDR: it kinda works, indeed fixes the "polonius-imprecision/unnecessary_error" test (but ofc fails the "polonius-imprecision/flow_sensitive_equality_required" case causing the 2nd version to exist). However, 2 rustc tests fail when trying it out for real (2 cases which are expected to fail but do compile)

lqd (Sep 20 2019 at 17:19, on Zulip):

version 2, derived from Niko's 2nd comment: "flow sensitive equality". TLDR: indeed passes the "polonius-imprecision/flow_sensitive_equality_required" case but works a bit less overall for now, as it eg fails on the "polonius-imprecision/cycle_unification" test where it doesn't detect the error, which I hadn't noticed before. Trying it out in rustc, 16 tests fail (a mix of tests which shouldn't compile but do, and others with less errors than expected) including both from the previous version.

lqd (Sep 20 2019 at 17:21, on Zulip):

so the plan is to locate the source of the 2 errors of v1, because it seems related to equality rather than its flow-sensitivity or lack thereof (or a mistake in both versions), and debug/understand why v2 fails to find the error on "cycle_unification"

Albin Stjerna (Sep 20 2019 at 18:54, on Zulip):

I cleaned up the equality prototype a bit, as it used to rely on features of my datafrog fork, and rebased over master

Is there a reason why you can't merge your Datafrog fork?

Albin Stjerna (Sep 20 2019 at 18:54, on Zulip):

(I assume there is, but I'm curious)

lqd (Sep 20 2019 at 18:57, on Zulip):

it's mostly in an experimental state, there's no reason per se, rather than needing to do the work to complete / reject the experiments. in this case it was about having 1 leaper (easy to upstream if needed, but not super important) and dumping all the tuples datafrog creates à la datalog provenance but done cheaply

lqd (Sep 20 2019 at 19:00, on Zulip):

(I mentioned this because if someone checked out the previous branch it wouldn't build without a bit of massaging — which I've done in the new one)

lqd (Sep 21 2019 at 09:55, on Zulip):

I think figured out problem 2: flow sensitive equality was dependent on liveness across edges (like the requires relation) but it shouldn’t IIUC, with that fixed it should work the on cycle_unification test case (funnily enough, that rule could now use Leapers of size 1 :)

lqd (Sep 23 2019 at 15:03, on Zulip):

Niko: I think we want to be able to say that the polonius loop "computes" the set of loans represented by each origin at each point

for a "minimal subset" of loans/origins/points actually needed to detect errors, right ?

lqd (Sep 25 2019 at 00:22, on Zulip):

also this begs the question @nikomatsakis, if we had to choose between 1) what we have today with the "unnecessary_error" caveat that NLL also has, or 2) the prototype as initially described in issue #120 with the "flow_sensitive_equality_required" caveat from the second comment, and that option 1 doesn't have but NLL has, or 3) "flow sensitive equality" as the solution to both previous options caveats with the doubts that flow-sensitivity may be hard to pull off, what would we choose ? :)

lqd (Sep 25 2019 at 00:25, on Zulip):

(by "may be hard to pull off" I mean 50-500k equality tuples flowing through 50k+ CFGs is slow rn)

lqd (Sep 25 2019 at 00:27, on Zulip):

(maybe just buggy :)

lqd (Sep 25 2019 at 01:02, on Zulip):

(deleted)

nikomatsakis (Oct 01 2019 at 19:17, on Zulip):

I refuse to choose :P

nikomatsakis (Oct 01 2019 at 19:18, on Zulip):

I can't really understand why equality tuples should be harder than the subset tuples we had before

nikomatsakis (Oct 01 2019 at 19:18, on Zulip):

Something is confusing to me

lqd (Oct 01 2019 at 19:35, on Zulip):

maybe it's doing the TC before propagating it, but something is fishy indeed

lqd (Oct 01 2019 at 19:36, on Zulip):

I'll look more into it

lqd (Oct 01 2019 at 19:38, on Zulip):

or better utilizing the fact that equality is symmetric as right now we'll have both values in the facts

lqd (Oct 01 2019 at 19:39, on Zulip):

stomping fist on table I shall investigate !

lqd (Oct 10 2019 at 10:48, on Zulip):

here's the data I mentioned tuesday:
- the MIR,
- a filtered graphviz file output to remove the liveness facts cause they're not the problem here (but which reminds me see we still keep in-memory even after computing it, and we'll solve when moving to a more pipeline-ish process).
- note that the source is this where I've removed type ascription to simplify the MIR and remove a bunch of facts

the missed error is at bb10[0], and the live loan is "L1": bw1; so we can ignore all the L0 and L2 facts (I can filter them out of the graphviz if need be), the origin we're interested in is '11

lqd (Oct 10 2019 at 11:02, on Zulip):

we can see that '11 is equated with '16 at bb7[3], itself being equated to '19 at bb7[10]. L1 is in '9, '19, '20, '23 at the call site, and none of those will be live at the error site

lqd (Oct 10 2019 at 11:07, on Zulip):

(L1 is mostly in '17 from its creation (bb7[6]) until just before the call at bb7[12] where it flows into '20)

lqd (Oct 10 2019 at 11:22, on Zulip):

(I'll add equality tuples to the graphviz, it's not clear enough otherwise)

lqd (Oct 10 2019 at 11:49, on Zulip):

what usually happens: '11 and '16 are joined in equality by '19 at bb7[10], where '16 dies; at the call site '20 flows in '9, then '19 and into '11 which we wanted

lqd (Oct 10 2019 at 11:53, on Zulip):

here there should be an equality TC at bb7[10] otherwise that link is lost

lqd (Oct 10 2019 at 12:37, on Zulip):

(I'm back I had to go buy a house :p)

lqd (Oct 10 2019 at 13:25, on Zulip):

and with that, we're back in business

lqd (Oct 10 2019 at 13:28, on Zulip):

(I can't really test clap, there's no data in the repo anymore since liveness landed; I'll try to add that back and then test it out; and run rustc's tests as well)

lqd (Oct 10 2019 at 15:45, on Zulip):

rustc results: a couple more OOM/huge memory uses (some possibly unrelated to this variant, where other variants seem to also use a lot of memory, and could bypass the problem via location insensitivity; and others which only happend with the prototype), 2 cases which now start compiling:
- first, borrowck/mut-borrow-in-loop.rs: borrowing in an infinite loop, and which seems unclear to me from a cursory look (like, it seems the loan could only last for the call and not continue into the next iteration ?)
- and nll/promoted-bounds.rs which feels like it shouldn't compile tho :p

lqd (Oct 10 2019 at 22:07, on Zulip):

apart from that, here's how it looks with help from the datapond generator (and manually converted to leapjoins, indices removed, etc), and perf seems ok (with interesting-ness filtering ofc)

Matthew Jasper (Oct 15 2019 at 19:14, on Zulip):

Both examples should fail to compile. The functions in the loops have to borrow the reference for 'abecause of their types (although it's pretty hard to make a function pointer where this is a problem).

lqd (Oct 15 2019 at 19:15, on Zulip):

thanks @Matthew Jasper I'll analyze those in more detail then and see where the rules break down

Last update: Nov 15 2019 at 20:35UTC