Stream: t-compiler/wg-polonius

Topic: meeting 2019.10.08


lqd (Oct 08 2019 at 18:58, on Zulip):

early :wave:

lqd (Oct 08 2019 at 19:00, on Zulip):

hello friends from @WG-polonius :)

nikomatsakis (Oct 08 2019 at 19:00, on Zulip):

I've been catching up on this stream in last few minutes

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

I know y'all have been busy with life and things and presentations :)

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

nice announcement: Matthew's PR #64749 has landed :)

nikomatsakis (Oct 08 2019 at 19:02, on Zulip):

Also I merged https://github.com/rust-lang/polonius/pull/127

nikomatsakis (Oct 08 2019 at 19:02, on Zulip):

uh..just now

lqd (Oct 08 2019 at 19:02, on Zulip):

nice, thanks niko

lqd (Oct 08 2019 at 19:02, on Zulip):

I have been reading your RBR presentation and my biased opinion is: I love it

nikomatsakis (Oct 08 2019 at 19:02, on Zulip):

great :)

nikomatsakis (Oct 08 2019 at 19:03, on Zulip):

that reminds me

nikomatsakis (Oct 08 2019 at 19:03, on Zulip):

I want to do a dry run soon-ish

nikomatsakis (Oct 08 2019 at 19:03, on Zulip):

I've probably got a bit more material I want to cover, not sure quite where to draw the line

nikomatsakis (Oct 08 2019 at 19:03, on Zulip):

I am very unsure how long it will take

nikomatsakis (Oct 08 2019 at 19:03, on Zulip):

and if I am going into too much detail on some things (the answer to that, I find, is usually no but...)

nikomatsakis (Oct 08 2019 at 19:03, on Zulip):

I would like to at least cover named lifetimes a bit and show why polonius helps with "Problem Case #3"

nikomatsakis (Oct 08 2019 at 19:03, on Zulip):

I probably won't get to killed loans

lqd (Oct 08 2019 at 19:04, on Zulip):

makes sense

lqd (Oct 08 2019 at 19:04, on Zulip):

how long is the presentation btw ?

nikomatsakis (Oct 08 2019 at 19:04, on Zulip):

I think 30 minutes

lqd (Oct 08 2019 at 19:04, on Zulip):

oh

nikomatsakis (Oct 08 2019 at 19:05, on Zulip):

so yeah it can't be too long :)

lqd (Oct 08 2019 at 19:05, on Zulip):

just holla if you need someone to listen to a dry run

lqd (Oct 08 2019 at 19:05, on Zulip):

(unsure if that's how it's spelled ?)

nikomatsakis (Oct 08 2019 at 19:05, on Zulip):

"holla"?

lqd (Oct 08 2019 at 19:05, on Zulip):

lol

lqd (Oct 08 2019 at 19:05, on Zulip):

just ask/ping

nikomatsakis (Oct 08 2019 at 19:05, on Zulip):

I knew what you meant ;)

lqd (Oct 08 2019 at 19:05, on Zulip):

:)

nikomatsakis (Oct 08 2019 at 19:06, on Zulip):

I should try to schedule one -- having a date would probably be good

lqd (Oct 08 2019 at 19:06, on Zulip):

it's cool to see this make progress as well

nikomatsakis (Oct 08 2019 at 19:06, on Zulip):

(maybe Friday?)

lqd (Oct 08 2019 at 19:06, on Zulip):

sure

lqd (Oct 08 2019 at 19:06, on Zulip):

as for myself this week, as I had been working on demand transformation before and found it hard to test changes

lqd (Oct 08 2019 at 19:07, on Zulip):

as it requires spending a bit of time coding the new rules in datafrog

lqd (Oct 08 2019 at 19:07, on Zulip):

I have this week finished my first rev of the "skeleton compiler/generator"

nikomatsakis (Oct 08 2019 at 19:07, on Zulip):

I saw the comments on zulip, very neat

lqd (Oct 08 2019 at 19:07, on Zulip):

I initially opened a PR on polonius (as it was for dogfooding there) but indeed it was not the right place

lqd (Oct 08 2019 at 19:07, on Zulip):

so it's at https://github.com/lqd/datapond until stable enough to be upstreamed in datafrog say

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

but it can handle the naive rules, flow sensitive equality, and the DTs I've done

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

so very helpful to me

nikomatsakis (Oct 08 2019 at 19:08, on Zulip):

very cool

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

I've also been working on said flow sensitive equality, and if you have a few minutes I hoped we could talk a bit about that

nikomatsakis (Oct 08 2019 at 19:09, on Zulip):

yeah

lqd (Oct 08 2019 at 19:09, on Zulip):

as I have more data to give you an intuition about what I meant

lqd (Oct 08 2019 at 19:09, on Zulip):

so basically my issue is about propagating equality

lqd (Oct 08 2019 at 19:09, on Zulip):

and esp wrt liveness

lqd (Oct 08 2019 at 19:09, on Zulip):

in the other variant we only propagate subsets and containment in the cfg when origins are live

lqd (Oct 08 2019 at 19:10, on Zulip):

for the flow sensitive equality, I've done both with and without limiting with liveness

lqd (Oct 08 2019 at 19:11, on Zulip):

for most simple cases and benchmarks this works similarly

lqd (Oct 08 2019 at 19:11, on Zulip):

however

lqd (Oct 08 2019 at 19:11, on Zulip):

if I propagate equality throughout it works on all rustc tests, etc but clap doesn't work

lqd (Oct 08 2019 at 19:11, on Zulip):

where doesn't work means it'll take a loooong time

lqd (Oct 08 2019 at 19:12, on Zulip):

why: there are 600K equal tuples, needing to be propagated through a 50k CFG

lqd (Oct 08 2019 at 19:12, on Zulip):

worst case (all equal tuples being at the start of the cfg, which is not the case in clap, but say) that's 200GB+

nikomatsakis (Oct 08 2019 at 19:12, on Zulip):

so why are there 600K equal tuples

nikomatsakis (Oct 08 2019 at 19:12, on Zulip):

let me back up one sec

nikomatsakis (Oct 08 2019 at 19:13, on Zulip):

because Ihave a question

nikomatsakis (Oct 08 2019 at 19:13, on Zulip):

you mentioned "liveness"

lqd (Oct 08 2019 at 19:13, on Zulip):

right

nikomatsakis (Oct 08 2019 at 19:13, on Zulip):

I think that equality tuples -- like our subset tuples -- could be constrained by liveness

nikomatsakis (Oct 08 2019 at 19:13, on Zulip):

is that 600K taking that into account?

lqd (Oct 08 2019 at 19:13, on Zulip):

yeah that's my other half of the writeup, if liveness is taken into account this is all acceptable

lqd (Oct 08 2019 at 19:14, on Zulip):

assuming we heavily filter like we mentioned before

lqd (Oct 08 2019 at 19:14, on Zulip):

only track the invalidated loans, and the origins they flow into, etc

lqd (Oct 08 2019 at 19:14, on Zulip):

however

nikomatsakis (Oct 08 2019 at 19:14, on Zulip):

ok, but I want to now understand why there are more "equality" tuples than "subset" tuples

lqd (Oct 08 2019 at 19:14, on Zulip):

there aren't more tuples

nikomatsakis (Oct 08 2019 at 19:14, on Zulip):

I do think we want to filter but I don't think we should have to filter

lqd (Oct 08 2019 at 19:14, on Zulip):

it's just 90% of the subsets

nikomatsakis (Oct 08 2019 at 19:14, on Zulip):

ok; clap was also very slow with naive rules before

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

yeah

nikomatsakis (Oct 08 2019 at 19:15, on Zulip):

so is it just that you're comparing naive rules against datafrog-opt?

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

with the filtering I mentioned it's super fast on naive now

nikomatsakis (Oct 08 2019 at 19:16, on Zulip):

it's just 90% of the subsets

it also feels like we should be able to leverage union-find here

nikomatsakis (Oct 08 2019 at 19:16, on Zulip):

as an aside

lqd (Oct 08 2019 at 19:16, on Zulip):

(yeah probably)

lqd (Oct 08 2019 at 19:16, on Zulip):

the interesting I found out was: if we constraint equality propagation to respect liveness

lqd (Oct 08 2019 at 19:16, on Zulip):

another simple case (which I'll link in a sec) stops working

lqd (Oct 08 2019 at 19:16, on Zulip):

and 16 out of the 9K rustc tests

lqd (Oct 08 2019 at 19:17, on Zulip):

here https://github.com/lqd/borrow-check/blob/variant_prototype2/inputs/polonius-imprecision/polonius-imprecision.rs#L24-L36

lqd (Oct 08 2019 at 19:17, on Zulip):

the loan which should be live until the += will stop at the p.push(q); line if we limit it to liveness

lqd (Oct 08 2019 at 19:18, on Zulip):

it works with full propagation, all existing variants, and even static equality, but not flow sensitive equality + liveness

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

the loan which should be live until the += will stop at the p.push(q); line if we limit it to liveness

so we get no error?

lqd (Oct 08 2019 at 19:18, on Zulip):

indeed

nikomatsakis (Oct 08 2019 at 19:19, on Zulip):

curious. this sounds like the bug has to do with the "transitive" part of the rules

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

the transitive rules are only transitive at a specific point

nikomatsakis (Oct 08 2019 at 19:19, on Zulip):

so specifically, the naive rules

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

so maybe some subsets should still be propagated

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

in addition to equality

nikomatsakis (Oct 08 2019 at 19:19, on Zulip):

compute the transition subset/contains relations (or whatever names we use for those...)

nikomatsakis (Oct 08 2019 at 19:20, on Zulip):

such that when you kill an origin in the middle (because it's no longer live), its effects are propagated

lqd (Oct 08 2019 at 19:20, on Zulip):

there's also a similar mechanism in the opt rules IIRC

nikomatsakis (Oct 08 2019 at 19:21, on Zulip):

my expectation would be that the p.push(q) call -- on entry to the mid-point, p is live

nikomatsakis (Oct 08 2019 at 19:21, on Zulip):

as is v

nikomatsakis (Oct 08 2019 at 19:21, on Zulip):

and hence we add L0 to 'p, which is equated with 'v

nikomatsakis (Oct 08 2019 at 19:21, on Zulip):

and so 'v winds up including L0

nikomatsakis (Oct 08 2019 at 19:21, on Zulip):

later, 'p goes dead, but 'v still includes L0

nikomatsakis (Oct 08 2019 at 19:21, on Zulip):

does that make sense?

lqd (Oct 08 2019 at 19:22, on Zulip):

oh it does

lqd (Oct 08 2019 at 19:22, on Zulip):

I don't have my complete notes with me but

lqd (Oct 08 2019 at 19:22, on Zulip):

I'll gather some more data to show exactly the facts we get

lqd (Oct 08 2019 at 19:23, on Zulip):

interning is messing my notes since it's different between machines

lqd (Oct 08 2019 at 19:23, on Zulip):

but in the other rules here I think a regular subset maintains the "containment" through this terminator to the next block, and in the prototype I don't have such a mechanism

lqd (Oct 08 2019 at 19:24, on Zulip):

(because we wanted to avoid tracking subsets along the cfg, only equality)

nikomatsakis (Oct 08 2019 at 19:24, on Zulip):

do you have a ptr to the rules I can review?

lqd (Oct 08 2019 at 19:25, on Zulip):

yeah I think https://github.com/lqd/datapond/blob/master/examples/generate_skeleton.rs

lqd (Oct 08 2019 at 19:26, on Zulip):

R4 is the one where liveness coming into play has the effect I'm talking about

lqd (Oct 08 2019 at 19:26, on Zulip):

in the link there is no liveness filtering, so it's the case where clap blows up but everything "works" otherwise

lqd (Oct 08 2019 at 19:27, on Zulip):

(no mentioning the inefficiency of "containment" with both subsets and equality, which are almost the same data in clap; that is R1 and R5 being the same thing locally at a given point when not talking about propagation through the cfg)

nikomatsakis (Oct 08 2019 at 19:28, on Zulip):

/me reading

nikomatsakis (Oct 08 2019 at 19:30, on Zulip):

if you were to incorporate liveness, would it look like

      // R4
        equals(O1, O2, Q) :-
          equals(O1, O2, P),
          cfg_edge(P, Q),
          region_live_at(O1, Q),
          region_live_at(O2, Q).

but be otherwise identical, @lqd ?

lqd (Oct 08 2019 at 19:30, on Zulip):

exactly

lqd (Oct 08 2019 at 19:31, on Zulip):

(and just filtering on O1 or O2's liveness will result in the same behaviour)

nikomatsakis (Oct 08 2019 at 19:32, on Zulip):

curious

nikomatsakis (Oct 08 2019 at 19:32, on Zulip):

well, I guess it'd be good if you had some idea of the tuples

nikomatsakis (Oct 08 2019 at 19:32, on Zulip):

do you have the input fact set from the example?

lqd (Oct 08 2019 at 19:32, on Zulip):

I do but will gather it completely for you

lqd (Oct 08 2019 at 19:32, on Zulip):

the summarized data I mean (annotated mir)

lqd (Oct 08 2019 at 19:32, on Zulip):

the data is in the repo just a sec

lqd (Oct 08 2019 at 19:33, on Zulip):

https://github.com/lqd/borrow-check/tree/variant_prototype2/inputs/polonius-imprecision/nll-facts/cycle_unification

lqd (Oct 08 2019 at 19:33, on Zulip):

I'd love a -Zdump-mir=polonius annotated with facts tbh :)

Albin Stjerna (Oct 08 2019 at 19:34, on Zulip):

That thought has crossed my mind too

nikomatsakis (Oct 08 2019 at 19:34, on Zulip):

yeah :)

nikomatsakis (Oct 08 2019 at 19:34, on Zulip):

The NLL annotation mechanisms are kinda nice

nikomatsakis (Oct 08 2019 at 19:34, on Zulip):

wouldn't be too hard to add

nikomatsakis (Oct 08 2019 at 19:34, on Zulip):

I feel like... I even made one at some point

lqd (Oct 08 2019 at 19:34, on Zulip):

reallllllyyyy ??? ;)

nikomatsakis (Oct 08 2019 at 19:34, on Zulip):

maybe not for polonius

nikomatsakis (Oct 08 2019 at 19:35, on Zulip):

I remember looking at MIR annotated with e.g. the subset relations created at each point

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

nice

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

we'll get it done

nikomatsakis (Oct 08 2019 at 19:35, on Zulip):

well I can't really debug from that base output:)

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

exactly

nikomatsakis (Oct 08 2019 at 19:35, on Zulip):

I guess I'd have to try running it

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

I'll finish annotating the MIR I have already begun in any case

nikomatsakis (Oct 08 2019 at 19:36, on Zulip):

didn't we have some kind of graphviz output from polonius too?

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

we do yeah

nikomatsakis (Oct 08 2019 at 19:36, on Zulip):

I dont' quite recall what it looked like :)

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

--graphviz-file

lqd (Oct 08 2019 at 19:37, on Zulip):

it's helpful but I think there's some output facts in there

lqd (Oct 08 2019 at 19:37, on Zulip):

I've added some provenance info in dafrog and it's been invaluable for these cases

nikomatsakis (Oct 08 2019 at 19:37, on Zulip):

this would probably be more of a "lack of provenance"

nikomatsakis (Oct 08 2019 at 19:37, on Zulip):

but I can imagine

nikomatsakis (Oct 08 2019 at 19:38, on Zulip):

i.e., we're missing elements

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

now of course as I needed to understand why tuples weren't being propagated, I really need why-not-provenance

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

right

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

which is less easy than a println for provenance :joy:

nikomatsakis (Oct 08 2019 at 19:38, on Zulip):

in any case I think the main thing we would want to know (to start) is the requires relation at the point of call

Albin Stjerna (Oct 08 2019 at 19:38, on Zulip):

I have to go, but I'll just say my one thing: yay, great renaming has landed, I'll try to start from there on the initialisation. Also, Tobias finally subject reviewed my thesis and he had...some comments, decreasing P(time to work on initialisation). Sorry for interrupting!

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

awesome @Albin Stjerna :)

nikomatsakis (Oct 08 2019 at 19:39, on Zulip):

oh btw

nikomatsakis (Oct 08 2019 at 19:39, on Zulip):

there is something else

nikomatsakis (Oct 08 2019 at 19:39, on Zulip):

i'm co-organizing a workshop at ETAPS 2020

nikomatsakis (Oct 08 2019 at 19:39, on Zulip):

https://sites.google.com/view/rustverify2020

nikomatsakis (Oct 08 2019 at 19:40, on Zulip):

we were thinking of having an invited talk on polonius

lqd (Oct 08 2019 at 19:40, on Zulip):

in any case I think the main thing we would want to know (to start) is the requires relation at the point of call

I'll get all this data, I mostly wanted to mention this in case y'all had ideas about liveness and equality propagation. at least I hope I was able to give some intuition in what I've been seeing

nikomatsakis (Oct 08 2019 at 19:40, on Zulip):

and I wanted to see whether @lqd and @Albin Stjerna how much you'd want to be involved :)

nikomatsakis (Oct 08 2019 at 19:40, on Zulip):

(and/or if you want to give it)

nikomatsakis (Oct 08 2019 at 19:40, on Zulip):

it's not until April

nikomatsakis (Oct 08 2019 at 19:40, on Zulip):

something to mull over :)

lqd (Oct 08 2019 at 19:41, on Zulip):

I can help for sure (maybe not give it :p)

Albin Stjerna (Oct 08 2019 at 19:41, on Zulip):

I have no idea what I can do for now, but I'll try to figure something out in the mean time!

nikomatsakis (Oct 08 2019 at 19:41, on Zulip):

we got some time to think it over

lqd (Oct 08 2019 at 19:41, on Zulip):

where "for sure" == I'm not sure how, but will lend a hand for whatever is needed

nikomatsakis (Oct 08 2019 at 19:41, on Zulip):

ps @lqd great work

lqd (Oct 08 2019 at 19:42, on Zulip):

also to matthew :)

nikomatsakis (Oct 08 2019 at 19:42, on Zulip):

very true! that PR was epic

lqd (Oct 08 2019 at 19:42, on Zulip):

thank you :)

Albin Stjerna (Oct 08 2019 at 19:42, on Zulip):

Honestly, I'm happy to have any excuse go give my supervisor for keeping working on Polonius :)

lqd (Oct 08 2019 at 19:42, on Zulip):

still a lot more work to do but we're making progress

nikomatsakis (Oct 08 2019 at 19:42, on Zulip):

and I wanted to see whether lqd and Albin Stjerna how much you'd want to be involved :)

and yes I actually did mean to ask @Matthew Jasper the same :)

nikomatsakis (Oct 08 2019 at 19:42, on Zulip):

which reminds me, did we add them to the team repo yet?

nikomatsakis (Oct 08 2019 at 19:43, on Zulip):

if not, let me do that...

lqd (Oct 08 2019 at 19:43, on Zulip):

I think only admins can know this

lqd (Oct 08 2019 at 19:43, on Zulip):

right ?

nikomatsakis (Oct 08 2019 at 19:44, on Zulip):

https://github.com/rust-lang/team/pull/139

lqd (Oct 08 2019 at 19:44, on Zulip):

but in any case sorry for running long it's been really fun

lqd (Oct 08 2019 at 19:44, on Zulip):

I'll gather more data this week to make sure everything's clear

nikomatsakis (Oct 08 2019 at 19:45, on Zulip):

I wonder if I can arrange to take a week and just do polonius :)

nikomatsakis (Oct 08 2019 at 19:45, on Zulip):

/me daydreams

lqd (Oct 08 2019 at 19:45, on Zulip):

sounds unlikely :)

lqd (Oct 08 2019 at 19:46, on Zulip):

maybe after RBR an hour here and there could be doable

lqd (Oct 08 2019 at 19:46, on Zulip):

btw if any of you are going to rustfest barcelona in november, I will be seeing you there

Albin Stjerna (Oct 08 2019 at 19:47, on Zulip):

Nope, but I am going to SPLASH in a few weeks

lqd (Oct 08 2019 at 19:47, on Zulip):

(and if that's all we have, thanks a lot everyone :wave:)

Albin Stjerna (Oct 08 2019 at 19:48, on Zulip):

Thanks!

nikomatsakis (Oct 08 2019 at 19:51, on Zulip):

Nope, but I am going to SPLASH in a few weeks

oh, really? man, I was almost going to go, but I think i'm not now

nikomatsakis (Oct 08 2019 at 19:51, on Zulip):

I just couldn't make the travel work

nikomatsakis (Oct 08 2019 at 19:51, on Zulip):

but you're the second person i've heard who's going that I'd love to catch up with

nikomatsakis (Oct 08 2019 at 19:51, on Zulip):

/me contemplates last minute trips

lqd (Oct 08 2019 at 19:51, on Zulip):

and it's in Athens ?!

Albin Stjerna (Oct 08 2019 at 20:01, on Zulip):

Yes, it is

Albin Stjerna (Oct 08 2019 at 20:03, on Zulip):

I'll be a student volunteer

lqd (Oct 09 2019 at 08:29, on Zulip):

it also feels like we should be able to leverage union-find here

to bounce back on this, receiving the SCCs would indeed help in some cases, and equality tuples in general (as now they are sometimes materialized all over the CFG, and are the source of the OOMs)

lqd (Oct 09 2019 at 08:32, on Zulip):

I've also noticed type ascriptions generating a lot of facts: these 10 lines (of course it's sugar-y) generate 3200 outlives facts; so just looking at the size of the facts for this simple example, there could be some opportunities there as well

Last update: Nov 15 2019 at 20:55UTC