Stream: t-compiler/wg-polonius

Topic: meeting 2019.10.01


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

hello :)

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

/me hides in shame, because he hasn't had any time for polonius lately

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

:)

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

this week Matthew made this cool PR https://github.com/rust-lang/rust/pull/64749

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

which fixes the last failure in the test suite (not the OOMs)

Albin Stjerna (Oct 01 2019 at 19:02, on Zulip):

/me hides in shame, because he hasn't had any time for polonius lately

SAME

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

computing which things outlive free regions as a liveness optimization is interesting since liveness is also done in polonius

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

I wonder if that affects things or not, speed-wise

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

at least reducing some of the variables we compute liveness in polonius, I think ?

Albin Stjerna (Oct 01 2019 at 19:05, on Zulip):

I think liveness is sort of computed before regions/origins/provenances enters into the equation

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

there seems to be an NLL fix in there as well, even though the PR text only mentions Polonius, but I could be interpreting things wrong

Albin Stjerna (Oct 01 2019 at 19:06, on Zulip):

So the main point of optimisation should probably be to stop computing liveness for variables that are neither structs with (structs with...) references or holding references themselves

Albin Stjerna (Oct 01 2019 at 19:06, on Zulip):

Or, not to even emit those into Polonius in the first place

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

some of this is done in rustc but was disabled because it broke polonius

Albin Stjerna (Oct 01 2019 at 19:07, on Zulip):

@lqd Is this in the "test difference" PR you mean?

Albin Stjerna (Oct 01 2019 at 19:07, on Zulip):

Or are you referring to some other PR?

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

So NLL does this same optimization

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

basically for the same reason

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

this PR re-enables it (now that I think liveness takes care of that)

Albin Stjerna (Oct 01 2019 at 19:07, on Zulip):

Aaah ok

Albin Stjerna (Oct 01 2019 at 19:07, on Zulip):

Cool!

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

and at the same time fixes the overflow in generating drop facts during fact generation

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

I sort of imaged that eventually we would want to do this analysis in polonius

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

(but I think it makes sense to do in rustc for now, and maybe forever)

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

(which is what you and Matthew talked about before Albin IIRC)

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

yeah, or maybe rustc and polonius would need to have a more interactive dialog when computing, to limit the number of facts to generate, etc

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

as for me, I've opened another inconsequential PR just to clean up some of the profiling data I had, and where interning in the polonius-bin was dominating the results

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

right, we might ship over some initial set of facts, etc

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

my one announcement is

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

I intend to start work in earnest on my RBR presentation this week

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

so maybe I'll try to draft some of you into suffering through a dry run or two

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

awesome

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

we'll see how much detail I want to do...

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

and also worked on generalizing the "interesting"-ness filtering by transforming the naive rules à la magic sets to be demand driven (there's some talk about that in another thread)

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

I've implemented these in datafrog (painful) but doesn't quite work yet (and maybe is flawed)

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

writing the rules being painful made me try to do a datalog to datafrog compiler as I mentioned there

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

so I have a tiny prototype of this, it doesn't setup data/relations/indices but can generate the (regular, not leapjoins) join/anti/map calls, etc

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

and obviously do the DT (Demand Transformation) from subsumtive tabling paper/thesis

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

(which seemed to work on the examples form the paper, but maybe not for us)

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

woah

Albin Stjerna (Oct 01 2019 at 19:13, on Zulip):

...that was kind of my reaction too

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

I've also worked on the OOMs just by emitting the materialized outlives on a different relation (à la outlives_everywhere but didn't modify the rules to take that into account)

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

I don't know if it's the right solution but at least I saw that a lot of those were equal as we assumed :)

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

haha <3

Tshepang Lekhonkhobe (Oct 01 2019 at 19:14, on Zulip):

I intend to start work in earnest on my RBR presentation this week

wasn't aware... looking forward to it https://rust-belt-rust.com/sessions/#polonius

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

I'm feeling doubtful with the flow-sensitive equality, I might be missing something but it might be hard to make it perform acceptably

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

very exciting

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

as I was saying in the dedicated topic

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

I plan to spent this afternoon reviewing, so I'll review @Matthew Jasper's PR, but let me know if there are other things that are more-or-less urgnt

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

very exciting

what is exciting ?

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

just all your updates :)

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

that typing came a bit late / out-of-sync with the rest of the conversation, sorry

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

I'm feeling doubtful with the flow-sensitive equality, I might be missing something but it might be hard to make it perform acceptably

I left some replies in the topic, but this definitely merits more work

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

there are a couple PRs to review in the polonius repo if you have some time (but probably more interesting ones already waiting on rustc :) like the renaming we mentioned seems done, etc

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

argh yeah

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

ok

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

I've got to see if I can dedicate at least an hour a week to polonius

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

seems like I should be able to squeeze that from somewhere :)

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

nothing major in any case

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

()but prob not till after RBR)

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

hopefully I'll have made more progress by then to have at least some things to review

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

there were some other datafrog-related things I mentioned in another dedicated topic, but I forgot if I haven't mentioned this last meeting tbh :)

Albin Stjerna (Oct 01 2019 at 19:21, on Zulip):

I think you didn't, at least not the code generation stuff

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

ah yes, mostly I meant the specialized relations we could do for our use-cases

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

eg bitsets/bloom filters for the killed relations etc

Albin Stjerna (Oct 01 2019 at 19:22, on Zulip):

Ah, I don't recall you mentioning them

Albin Stjerna (Oct 01 2019 at 19:22, on Zulip):

But I might have just forgotten :)

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

if anyone feels adventurous, they were here

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

and I think that's pretty much it :)

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

/me has been saving those for when he has a bit of time to read :)

Albin Stjerna (Oct 01 2019 at 19:23, on Zulip):

I guess when I finally start working on initialisation, I should start after the great renaming?

Albin Stjerna (Oct 01 2019 at 19:23, on Zulip):

I.e. merging the pull requests on my fork and going from there

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

this week I plan on finishing this tiny compiler so that writing rules is a bit easier, hopefully looking into demand-transformed rules and why they don't always work (and if that's a flaw in the approach or my derivation)

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

yeah I think so Albin, it's "just" needs reviewing/discussing otherwise

Albin Stjerna (Oct 01 2019 at 19:25, on Zulip):

Ok, so with any luck I will find some time to work on initialisation

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

but it might create annoyances otherwise; at least it's not blocking on the "what to do" part, more so the specifics of the code could have conflicts

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

this week I plan on finishing this tiny compiler so that writing rules is a bit easier, hopefully looking into demand-transformed rules and why they don't always work (and if that's a flaw in the approach or my derivation)

where is this compiler living?

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

and how do you invoke it?

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

I'd also like to see if the non-OOMy facts could easily map to the equal variant

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

right now it's a just a function in my polonius-bin repo

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

which is being invoked with a string of the rules, and it prints out the analysis and some rust code on stdout :p

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

a bit artisanal

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

ah ok :)

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

might eventually make a nice addition to datafrog, as a procedural macro or something

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

yeah

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

even though as I mentioned before maybe proc macro would hide the real code too much

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

seeing how often we try to optimize said code, removing indices, etc

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

maybe if I could spit a super query plan or something, but that seems unlikely

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

as it's suuuuuuuper hard and long to do :)

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

it shouldn't be too hard to get into a PR in the next couple weeks I think

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

(at least it could help a bit with prototyping rules, etc, more so than generating a perfectly formed computation one need not touch anymore)

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

if anyone has something else to add we're just on the 30mins mark :)

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

thanks @lqd

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

even though as I mentioned before maybe a proc macro would hide the real code too much

yeah this is why I've figured we'd hold off on those until now, but maybe we can get it smart enough

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

yeah

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

ah but thank you all for your time :) :wave:

Last update: Nov 15 2019 at 20:00UTC