Stream: t-compiler/wg-polonius

Topic: reboot meeting 2019.09.03


lqd (Sep 03 2019 at 19:02, on Zulip):

hello friends from @WG-polonius :) IIRC today should be the reboot meeting

nikomatsakis (Sep 03 2019 at 19:02, on Zulip):

Hola

lqd (Sep 03 2019 at 19:03, on Zulip):

I had posted a couple notes before here about my understanding / the current status of things I remember

lqd (Sep 03 2019 at 19:03, on Zulip):

I don't know if any of you had the time to read it (I know Albin has and made some comments)

lqd (Sep 03 2019 at 19:04, on Zulip):

but it lacked details on what they were working on, they know about it more than I do :)

Albin Stjerna (Sep 03 2019 at 19:05, on Zulip):

Excellent question!

lqd (Sep 03 2019 at 19:05, on Zulip):

@nikomatsakis did you want to know something in particular ? :)

lqd (Sep 03 2019 at 19:07, on Zulip):

at least I can give an update on what I have been doing since coming back from vacation: not much besides writing up these notes, and trying to better understand the structure of the OOM case I mentioned before (to assess "how problematic" it is)

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

sorry, just had a phone call come in

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

mm

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

let me skim those notes @lqd made but I guess I mostly wanted to kind of inventory the things that were going on and get resynchronized

lqd (Sep 03 2019 at 19:09, on Zulip):

@Albin Stjerna are you still stuck on move errors btw ? (since I think you commented about that in the notes)

nikomatsakis (Sep 03 2019 at 19:09, on Zulip):

one thing I think is maybe missing from your list, @lqd, is the potential changes to make polonius more precise, right? I'm trying to remember if we had a pithy name for those

nikomatsakis (Sep 03 2019 at 19:09, on Zulip):

basically not propagating the full subset, but only "equality"

lqd (Sep 03 2019 at 19:09, on Zulip):

it's a bit down in the doc

nikomatsakis (Sep 03 2019 at 19:09, on Zulip):

oh wait

nikomatsakis (Sep 03 2019 at 19:09, on Zulip):

that's under the II section

lqd (Sep 03 2019 at 19:09, on Zulip):

right

Albin Stjerna (Sep 03 2019 at 19:10, on Zulip):

Err, I have a preliminary idea for something that would probably work, but it's literally in pencil in a notebook and I wrote it down at 3 am when I couldn't sleep last week

nikomatsakis (Sep 03 2019 at 19:10, on Zulip):

this list is really fantastic

Albin Stjerna (Sep 03 2019 at 19:10, on Zulip):

But I cut initialization errors from my thesis, and I want to finish it first

lqd (Sep 03 2019 at 19:10, on Zulip):

Matthew has looked into the last of the ui test suite failing test (an overflow in fact generation) and it should be easy to fix (and an optimisation IIUC) once Albin's work is done

nikomatsakis (Sep 03 2019 at 19:11, on Zulip):

OK. I've been doing a little bit of working on that "book" -- I think it's getting pretty important that we document better the rules, esp. as we talk about growing to other parts of the borrow check

lqd (Sep 03 2019 at 19:11, on Zulip):

agreed

Matthew Jasper (Sep 03 2019 at 19:11, on Zulip):

The run pass test is now a ui test, so it's not actually the last

nikomatsakis (Sep 03 2019 at 19:11, on Zulip):

Also, I unwisely agreed to give a presentation on Polonius for RustBeltRust :scared: so I thought it would be useful for me to try and work on how to explain things :)

Albin Stjerna (Sep 03 2019 at 19:11, on Zulip):

I'm actually working on is wrapping up a workable first draft of my thesis. My plan is to deliver it to my subject reviewer (and you! to the extent you have the time to look at it) on Monday, and before that I need:
- some light writing
- finish my re-run of the hackish Polonius-crater-monster-run that's been going for two weeks now (now with box plots) (async)
- figure out if I need to change the logic of var_maybe_initialized_at and if it still produces correct region_live_at if I go with the more precise analysis that @nikomatsakis suggested in their review of my PR

lqd (Sep 03 2019 at 19:12, on Zulip):

@Matthew Jasper it already was a UI test not a run-pass test IIRC ?

Matthew Jasper (Sep 03 2019 at 19:12, on Zulip):

I'm talking about the OoM in 1.2

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

@Matthew Jasper ah ok, yeah I think 2-3 of the run-pass cases were "interesting", maybe this one was the only hard blocker at the time

Albin Stjerna (Sep 03 2019 at 19:13, on Zulip):

Also, I'd be happy to cannibalise my thesis into the book of course

nikomatsakis (Sep 03 2019 at 19:14, on Zulip):

So @Albin Stjerna have you hacked up some more precise version of var_maybe_initialized_at? Would it be helpful to you to land the version we have and iterate?

nikomatsakis (Sep 03 2019 at 19:14, on Zulip):

I'd be ok with that

lqd (Sep 03 2019 at 19:14, on Zulip):

@nikomatsakis we can also help coming up with content for docs/book/rustbeltrust

Albin Stjerna (Sep 03 2019 at 19:15, on Zulip):

@nikomatsakis Good question

Albin Stjerna (Sep 03 2019 at 19:15, on Zulip):

The issue here really is that we don't have a reliable test suite

Albin Stjerna (Sep 03 2019 at 19:16, on Zulip):

So what I'd have to do is roll back the commit removing the region_live_at facts, try calculating it, comparing, and then moving on if it turns out to work

lqd (Sep 03 2019 at 19:16, on Zulip):

can we swap some part of rustc with $albinsThing and use rustc's test suites ?

Albin Stjerna (Sep 03 2019 at 19:16, on Zulip):

That would be nice

nikomatsakis (Sep 03 2019 at 19:16, on Zulip):

I'm confused

nikomatsakis (Sep 03 2019 at 19:17, on Zulip):

but it sounds a lot to me like we should land what we have

nikomatsakis (Sep 03 2019 at 19:17, on Zulip):

and then iterate

nikomatsakis (Sep 03 2019 at 19:17, on Zulip):

can we swap some part of rustc with $albinsThing and use rustc's test suites ?

like, isn't this what -Zpolonius does?

Albin Stjerna (Sep 03 2019 at 19:17, on Zulip):

Well, it might make sense to me

nikomatsakis (Sep 03 2019 at 19:17, on Zulip):

I mean I'm just generally in favor of getting things into master and out of PRs :)

nikomatsakis (Sep 03 2019 at 19:17, on Zulip):

as long as we open issues and track follow-up work ..

lqd (Sep 03 2019 at 19:18, on Zulip):

are we talking move analysis/liveness ?

Albin Stjerna (Sep 03 2019 at 19:18, on Zulip):

I know that what I have produces almost literally the same var_maybe_initialized_on_exit and literally the same region_live_as

Albin Stjerna (Sep 03 2019 at 19:18, on Zulip):

If that helps with the decision

nikomatsakis (Sep 03 2019 at 19:18, on Zulip):

We're talking specifically about https://github.com/rust-lang/polonius/pull/110

nikomatsakis (Sep 03 2019 at 19:19, on Zulip):

I think it's very close; I had a few suggestions for alternate formulations of the relations, which I would still like to pursue

lqd (Sep 03 2019 at 19:19, on Zulip):

yeah then the existing tests can be used ?

nikomatsakis (Sep 03 2019 at 19:19, on Zulip):

(but it's not very different)

Albin Stjerna (Sep 03 2019 at 19:19, on Zulip):

But maybe it makes sense, because regardless the iteration would happen in Polonius

Albin Stjerna (Sep 03 2019 at 19:19, on Zulip):

So we can merge my Rust PR

Albin Stjerna (Sep 03 2019 at 19:19, on Zulip):

But only after releasing a new Polonius

nikomatsakis (Sep 03 2019 at 19:19, on Zulip):

Uh, also true

nikomatsakis (Sep 03 2019 at 19:20, on Zulip):

I see, yeah, so we land your PR, land the rustc PR, and then we consider whether to tweak the rules (and we can compare the output after the changes to the output before, as well as of course running the rustc integration tests)

Albin Stjerna (Sep 03 2019 at 19:20, on Zulip):

Sounds good; I think they are a much better test for if things work than "does this change the input facts from what we had before"

nikomatsakis (Sep 03 2019 at 19:21, on Zulip):

Yes, ultimately the rustc integration tests are the best, though it's interesting to do the detailed comparison too

Albin Stjerna (Sep 03 2019 at 19:21, on Zulip):

They said, having never run the integration tests with Polonius

lqd (Sep 03 2019 at 19:21, on Zulip):

it would be nice to check if generating facts is faster with this PR

lqd (Sep 03 2019 at 19:21, on Zulip):

(as I think it should be)

nikomatsakis (Sep 03 2019 at 19:21, on Zulip):

OK, so, I'm happy to just land https://github.com/rust-lang/polonius/pull/110 now

Albin Stjerna (Sep 03 2019 at 19:21, on Zulip):

Good!

nikomatsakis (Sep 03 2019 at 19:22, on Zulip):

I will then assign myself a task to try and write something in the rust-book documenting it (because I want to :P)

nikomatsakis (Sep 03 2019 at 19:22, on Zulip):

which I think should then enable us to talk a bit about possible changes

nikomatsakis (Sep 03 2019 at 19:22, on Zulip):

in any case, those changes should be (largely?) local to polonius, since I think the facts rustc generates won't change (though I guess we might tweak something)

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

@nikomatsakis last time you mentioned wanting Polonius to be in "slow boil" mode, could you explain what you meant or what your plans were ? (since we're close to being out of time)

Albin Stjerna (Sep 03 2019 at 19:23, on Zulip):

I think so too

nikomatsakis (Sep 03 2019 at 19:23, on Zulip):

@Albin Stjerna did you update the PR with more extended comments on the input facts, like I mentioned?

nikomatsakis (Sep 03 2019 at 19:24, on Zulip):

@lqd by "slow boil" I meant roughly like what we're doing now -- that is, we're still making improvements, but we're not trying to spin up a big effort

Albin Stjerna (Sep 03 2019 at 19:24, on Zulip):

Let me check

nikomatsakis (Sep 03 2019 at 19:24, on Zulip):

we can also help coming up with content for docs/book/rustbeltrust

@lqd who was "we" here btw :)

lqd (Sep 03 2019 at 19:25, on Zulip):

I volunteer

nikomatsakis (Sep 03 2019 at 19:25, on Zulip):

one thing that would be good to try and write is to talk a bit about the inputs

lqd (Sep 03 2019 at 19:25, on Zulip):

(but probably other people can help of course)

nikomatsakis (Sep 03 2019 at 19:25, on Zulip):

this is to some extent commented in the source already

lqd (Sep 03 2019 at 19:26, on Zulip):

documenting how the inputs are generated would be nice

lqd (Sep 03 2019 at 19:26, on Zulip):

like you all did with the chalkification of rustc, describing how to lower to chalk rules etc

nikomatsakis (Sep 03 2019 at 19:26, on Zulip):

I think what would be good is

nikomatsakis (Sep 03 2019 at 19:27, on Zulip):

making some rust snippet and kind of using it to illustrate what each thing means

nikomatsakis (Sep 03 2019 at 19:27, on Zulip):

also, we should probably spend some effort getting our terminology good

nikomatsakis (Sep 03 2019 at 19:27, on Zulip):

hmm -- that might also want to be refactorings in the source

nikomatsakis (Sep 03 2019 at 19:27, on Zulip):

e.g. I was happy with "origin" for region -- I think that's what we agreed on? or was it provenance :stuck_out_tongue: ...

lqd (Sep 03 2019 at 19:27, on Zulip):

yeah I mentioned refactoring and terminology a bit in the notes as something that's partially decided on but not implemented

lqd (Sep 03 2019 at 19:28, on Zulip):

(what's everyone's availability for the "foreseeable future" btw ?)

Albin Stjerna (Sep 03 2019 at 19:29, on Zulip):

As I remember it we agreed on provenance?

Albin Stjerna (Sep 03 2019 at 19:29, on Zulip):

Or maybe I'm not getting the joke

nikomatsakis (Sep 03 2019 at 19:29, on Zulip):

looks like we said provenance, though I sort of like origin ;) well, we can bikeshed it. But I'd like to actually push those terms through the polonius codebase at least, and be consistent.

nikomatsakis (Sep 03 2019 at 19:29, on Zulip):

Or maybe I'm not getting the joke

the joke is more that we keep going back and forth :)

lqd (Sep 03 2019 at 19:29, on Zulip):

I'm still torn :)

nikomatsakis (Sep 03 2019 at 19:29, on Zulip):

and that I literally cannot remember :)

Albin Stjerna (Sep 03 2019 at 19:29, on Zulip):

Yes, we should also not have Hybrid execute the full initialisation and liveness analysis twice

Albin Stjerna (Sep 03 2019 at 19:30, on Zulip):

And a few other things

nikomatsakis (Sep 03 2019 at 19:30, on Zulip):

looks like we said provenance, though I sort of like origin ;) well, we can bikeshed it. But I'd like to actually push those terms through the polonius codebase at least, and be consistent.

the other thing to reconsider are the names for the various relations

nikomatsakis (Sep 03 2019 at 19:30, on Zulip):

e.g. I think maybe we still use "outlives" in some places etc

Albin Stjerna (Sep 03 2019 at 19:30, on Zulip):

Such as the outlives relation you mean?

nikomatsakis (Sep 03 2019 at 19:30, on Zulip):

right

lqd (Sep 03 2019 at 19:30, on Zulip):

renaming requiresto containsis the one I remember

Albin Stjerna (Sep 03 2019 at 19:30, on Zulip):

Also a few you suggested in the code review

Albin Stjerna (Sep 03 2019 at 19:30, on Zulip):

(I made notes of them)

Albin Stjerna (Sep 03 2019 at 19:31, on Zulip):

(what's everyone's availability for the "foreseeable future" btw ?)

Unknown, but I'll be able to answer properly in less than a month. I want to keep working on Polonius though because it's been fun

lqd (Sep 03 2019 at 19:32, on Zulip):

@Albin Stjerna thanks for the answer, glad to hear it :)

lqd (Sep 03 2019 at 19:32, on Zulip):

I don't know if I managed to convey that the "illegal subset relation errors" work and the "optimization" work are almost deadlocking each other

Albin Stjerna (Sep 03 2019 at 19:32, on Zulip):

Are they?

lqd (Sep 03 2019 at 19:33, on Zulip):

yeah, depending on the way to implement them, some data needs to be computed (or not)

Albin Stjerna (Sep 03 2019 at 19:33, on Zulip):

Oh I also have a flow chart of the entire analysis

Albin Stjerna (Sep 03 2019 at 19:33, on Zulip):

(spoilers for my thesis)

lqd (Sep 03 2019 at 19:33, on Zulip):

that data is the cause of polonius "slowness"

Albin Stjerna (Sep 03 2019 at 19:33, on Zulip):

In case that's useful for anything

Albin Stjerna (Sep 03 2019 at 19:33, on Zulip):

Ah, I see

lqd (Sep 03 2019 at 19:34, on Zulip):

the OOM case might be another concern, but impacting the current state, not the future

lqd (Sep 03 2019 at 19:35, on Zulip):

(maybe it's nothing to be concerned about and easily fixable, we'll see)

nikomatsakis (Sep 03 2019 at 19:35, on Zulip):

Oh I also have a flow chart of the entire analysis

neat

nikomatsakis (Sep 03 2019 at 19:35, on Zulip):

(sorry, was afk for a few minutes)

nikomatsakis (Sep 03 2019 at 19:36, on Zulip):

ok, well, this was a good meeting, I guess we have some next steps

?

lqd (Sep 03 2019 at 19:37, on Zulip):

SGTM

lqd (Sep 03 2019 at 19:37, on Zulip):

I guess we can talk about those other points I mentioned async

nikomatsakis (Sep 03 2019 at 19:37, on Zulip):

as for availability:

I'm not 100% sure how much time to devote to polonius, but I am quite determined that starting this week I'm going to be carving out some days to hack on rustc in general. I intend to focus on traits, but I think I will put some energy into polonius too, since I think both are pretty important.

Albin Stjerna (Sep 03 2019 at 19:38, on Zulip):

@nikomatsakis I have pushed the updates to all the facts now. I haven't written documentation for the var_initialized_at-calculating method yet.

nikomatsakis (Sep 03 2019 at 19:38, on Zulip):

yeah in particular I want to get the illegal subset relation + more precise analysis stuff figured out

nikomatsakis (Sep 03 2019 at 19:38, on Zulip):

nikomatsakis I have pushed the updates to all the facts now. I haven't written documentation for the var_initialized_at-calculating method yet.

I don't remember what docs I asked for but I think they can be moved to issues

Albin Stjerna (Sep 03 2019 at 19:38, on Zulip):

This one: https://github.com/rust-lang/polonius/pull/110#discussion_r318557584

lqd (Sep 03 2019 at 19:38, on Zulip):

awesome, good to hear Niko :)

Albin Stjerna (Sep 03 2019 at 19:38, on Zulip):

Sure, I'll make an issue right now

lqd (Sep 03 2019 at 19:40, on Zulip):

(I have forgotten to talk about my own availability: same as usual, I'm not ready to let go of Polonius either as I've spent a bunch of time on it and will love seeing it to fruition; of course, if other more pressing work is needed elsewhere, I can also devote my time to that)

Albin Stjerna (Sep 03 2019 at 19:41, on Zulip):

Also, it makes sense to wait I guess, because both the value of the relation it computes will probably change, _and_ it will probably be refactored into the general initialisation analysis and so have a different return value

Albin Stjerna (Sep 03 2019 at 19:41, on Zulip):

(there is an architectural decision waiting here I think)

lqd (Sep 03 2019 at 19:44, on Zulip):

(thanks everyone :wave: :)

Last update: Nov 15 2019 at 20:10UTC