Stream: t-compiler/wg-polonius

Topic: meeting 2019.03.14


nikomatsakis (Mar 14 2019 at 20:13, on Zulip):

Hello @WG-polonius !

nikomatsakis (Mar 14 2019 at 20:13, on Zulip):

Sorry i'm running late

nikomatsakis (Mar 14 2019 at 20:13, on Zulip):

we had our first lang team working group session today

nikomatsakis (Mar 14 2019 at 20:13, on Zulip):

and it ran over

nikomatsakis (Mar 14 2019 at 20:13, on Zulip):

Are people around?

Albin Stjerna (Mar 14 2019 at 20:14, on Zulip):

I am! Just barely, given that my internal clock is at 07:14 in the morning and I just pulled an all-nighter

nikomatsakis (Mar 14 2019 at 20:14, on Zulip):

Oh dear

Albin Stjerna (Mar 14 2019 at 20:14, on Zulip):

However, I am now back in Sweden

nikomatsakis (Mar 14 2019 at 20:15, on Zulip):

:tada:

nikomatsakis (Mar 14 2019 at 20:15, on Zulip):

Not that I have anything against Australia

nikomatsakis (Mar 14 2019 at 20:15, on Zulip):

But Sweden works better with my personal time zone ;)

nikomatsakis (Mar 14 2019 at 20:15, on Zulip):

So here is our Roadmap Paper Document

nikomatsakis (Mar 14 2019 at 20:15, on Zulip):

Let's quickly review where we're at

nikomatsakis (Mar 14 2019 at 20:16, on Zulip):

@Albin Stjerna implemented the hybrid sketch in polonius#102

nikomatsakis (Mar 14 2019 at 20:16, on Zulip):

@Matthew Jasper wrote mentoring instructions :tada:

nikomatsakis (Mar 14 2019 at 20:16, on Zulip):

I failed to do my tasks, mostly:

nikomatsakis (Mar 14 2019 at 20:16, on Zulip):

I sort of started on reviewing the PR though :)

nikomatsakis (Mar 14 2019 at 20:17, on Zulip):

but I guess we should figure out @Albin Stjerna what is a good next step, right? Do you feel like you are starting to understand how Polonius codebase is working?

Albin Stjerna (Mar 14 2019 at 20:17, on Zulip):

@nikomatsakis N.B the document you linked to is some sort of meetning minutes from 2019.03.14

nikomatsakis (Mar 14 2019 at 20:18, on Zulip):

whoops

nikomatsakis (Mar 14 2019 at 20:18, on Zulip):

fixed

nikomatsakis (Mar 14 2019 at 20:18, on Zulip):

I hope

Albin Stjerna (Mar 14 2019 at 20:18, on Zulip):

@nikomatsakis I feel like I understand it better than I did before, but I haven't fully grasped what every data structure does and how it interacts with datafrog yet

Albin Stjerna (Mar 14 2019 at 20:18, on Zulip):

But it's a good start, I think

nikomatsakis (Mar 14 2019 at 20:18, on Zulip):

So yes I was thinking about datafrog

nikomatsakis (Mar 14 2019 at 20:19, on Zulip):

Hmm

nikomatsakis (Mar 14 2019 at 20:19, on Zulip):

so I think one thing we could do

nikomatsakis (Mar 14 2019 at 20:19, on Zulip):

is to try to do a walk-through in which we connect the naive rules to their datafrog variants

nikomatsakis (Mar 14 2019 at 20:19, on Zulip):

that wouldn't really take much prep from my part and might be a nice piece of documentation to have

Albin Stjerna (Mar 14 2019 at 20:19, on Zulip):

That sounds like a good idea

nikomatsakis (Mar 14 2019 at 20:19, on Zulip):

we could try to do that (e.g.) tomorrow

nikomatsakis (Mar 14 2019 at 20:19, on Zulip):

but what is a good next task

nikomatsakis (Mar 14 2019 at 20:20, on Zulip):

I feel like we want to start trying to pivot towards deeper understanding of the rules themselves

Albin Stjerna (Mar 14 2019 at 20:20, on Zulip):

Yes, me too, because they are very abstract as they stand

nikomatsakis (Mar 14 2019 at 20:21, on Zulip):

I think polonius#102 looks good bw

nikomatsakis (Mar 14 2019 at 20:21, on Zulip):

I'm inclined to merge it

Albin Stjerna (Mar 14 2019 at 20:21, on Zulip):

I did skim the Static Program Analysis (Møller & Schwartzbach) on the plane(s), and I felt like that gave me some additional intuitions

nikomatsakis (Mar 14 2019 at 20:21, on Zulip):

One task we had talked about was to modify rustc

Albin Stjerna (Mar 14 2019 at 20:21, on Zulip):

Ok, so I'll drop the WIP then

nikomatsakis (Mar 14 2019 at 20:21, on Zulip):

I might rename my_xx to just xx

nikomatsakis (Mar 14 2019 at 20:22, on Zulip):

but that's just a nit

nikomatsakis (Mar 14 2019 at 20:22, on Zulip):

One task we had talked about was to modify rustc

i.e., to use this new hybrid

nikomatsakis (Mar 14 2019 at 20:22, on Zulip):

but I don't really think that's going to teach you a lot

nikomatsakis (Mar 14 2019 at 20:22, on Zulip):

might be a good task regardless, just to get you used to the rustc workflow a bit

nikomatsakis (Mar 14 2019 at 20:22, on Zulip):

it seems like maybe working with https://github.com/rust-lang/polonius/pull/99 (@lqd's PR) is a good next step

Albin Stjerna (Mar 14 2019 at 20:23, on Zulip):

I had it like that in my first version, but then I noticed that another variable shadows that one, which isn't a problem but I wasn't sure what best practices looked like so I went with a unique name

nikomatsakis (Mar 14 2019 at 20:23, on Zulip):

oh ok

nikomatsakis (Mar 14 2019 at 20:23, on Zulip):

I should look a bit more closely :)

nikomatsakis (Mar 14 2019 at 20:23, on Zulip):

hmm maybe an alternative would be

Albin Stjerna (Mar 14 2019 at 20:23, on Zulip):

Yes, I think so, and it might be a good way of giving me a feeling for How It All Fits Together

Albin Stjerna (Mar 14 2019 at 20:23, on Zulip):

The rustc integration, that is

nikomatsakis (Mar 14 2019 at 20:23, on Zulip):

yeah, so let's at least do that

Albin Stjerna (Mar 14 2019 at 20:24, on Zulip):

But what does that mean concretely, that rustc has an option to run the hybrid analysis on the fly?

nikomatsakis (Mar 14 2019 at 20:25, on Zulip):

Yes so right now

nikomatsakis (Mar 14 2019 at 20:25, on Zulip):

rustc has an option to use polonius, with the -Zpolonius flag (-Z are for unstable flags)

nikomatsakis (Mar 14 2019 at 20:25, on Zulip):

I don't recall which algorithm it uses by default, but I think you can use POLONIUS_ALGORITHM=foo to select

nikomatsakis (Mar 14 2019 at 20:25, on Zulip):

but I think hybrid is the right default choice

Albin Stjerna (Mar 14 2019 at 20:26, on Zulip):

Ah, OK, so a first-first step would be for me to figure out what it's currently doing, and then modifying that

nikomatsakis (Mar 14 2019 at 20:27, on Zulip):

yeo

nikomatsakis (Mar 14 2019 at 20:27, on Zulip):

this should be very easy in terms of the diff

Matthew Jasper (Mar 14 2019 at 20:27, on Zulip):

It will also need you to upgrade the polonius version

Albin Stjerna (Mar 14 2019 at 20:27, on Zulip):

Is there a benchmark collection anywhere by the way? It would be interesting to see how the hybrid compares to running the full analysis for something that actually needs the full analysis

nikomatsakis (Mar 14 2019 at 20:27, on Zulip):

we basically have to change this line

nikomatsakis (Mar 14 2019 at 20:27, on Zulip):

It will also need you to upgrade the polonius version

ah, good point

Albin Stjerna (Mar 14 2019 at 20:28, on Zulip):

Ah, so it becomes "Hybrid" in stead of "DatafrogOpt"

Albin Stjerna (Mar 14 2019 at 20:28, on Zulip):

For the default value

nikomatsakis (Mar 14 2019 at 20:28, on Zulip):

Is there a benchmark collection anywhere by the way? It would be interesting to see how the hybrid compares to running the full analysis for something that actually needs the full analysis

yes, so, we have perf.rust-lang.org, and a little while back @Santiago Pastorino went ahead and did some work to run polonius benchmarks, which I think we discussed in this Zulip topic

nikomatsakis (Mar 14 2019 at 20:28, on Zulip):

we should probably write out that procedure more carefully

nikomatsakis (Mar 14 2019 at 20:28, on Zulip):

it'd be nice to do the mesurements and confirm what we expect

nikomatsakis (Mar 14 2019 at 20:28, on Zulip):

we could add that as a "work item" for the week

Albin Stjerna (Mar 14 2019 at 20:29, on Zulip):

Yes, I think it's a good idea to start measuring early

Albin Stjerna (Mar 14 2019 at 20:29, on Zulip):

"You can only make as well as you measure"

Albin Stjerna (Mar 14 2019 at 20:29, on Zulip):

Also, the history might be interesting in itself

nikomatsakis (Mar 14 2019 at 20:30, on Zulip):

confirm

nikomatsakis (Mar 14 2019 at 20:30, on Zulip):

one nice thing would be if we include in the wg-polonius directory

nikomatsakis (Mar 14 2019 at 20:30, on Zulip):

a write-up of the steps to follow

nikomatsakis (Mar 14 2019 at 20:30, on Zulip):

I mean this directory: https://github.com/rust-lang/compiler-team/tree/master/working-groups/polonius

nikomatsakis (Mar 14 2019 at 20:30, on Zulip):

but it could also live on the rust-lang/polonius repo

nikomatsakis (Mar 14 2019 at 20:30, on Zulip):

somewhere\

nikomatsakis (Mar 14 2019 at 20:31, on Zulip):

I'd probably put it in the compiler-team repo, and we can also record measurements in a file in there

Albin Stjerna (Mar 14 2019 at 20:31, on Zulip):

Ah, with results you mean?

nikomatsakis (Mar 14 2019 at 20:31, on Zulip):

e.g., a little measurements directory

nikomatsakis (Mar 14 2019 at 20:31, on Zulip):

correct

nikomatsakis (Mar 14 2019 at 20:31, on Zulip):

(I'd like us to be using those directories to include "work products" from the work we're doing)

Albin Stjerna (Mar 14 2019 at 20:31, on Zulip):

How are the measurements currently taken?

nikomatsakis (Mar 14 2019 at 20:32, on Zulip):

there is a harness, that's why I linked to the zulip topic

nikomatsakis (Mar 14 2019 at 20:32, on Zulip):

I think it was explained in there what to do :)

Albin Stjerna (Mar 14 2019 at 20:32, on Zulip):

Ah, OK, then I can just start from there

nikomatsakis (Mar 14 2019 at 20:32, on Zulip):

the topic is called "finding perf spikes"

nikomatsakis (Mar 14 2019 at 20:32, on Zulip):

you could probably also ping @Santiago Pastorino for advice

nikomatsakis (Mar 14 2019 at 20:32, on Zulip):

(or the folks who were discussing in that topic)

nikomatsakis (Mar 14 2019 at 20:33, on Zulip):

ok, so we have two work items, I'm not sure how much time they will take, maybe enough, but I think we should be thinking about the next step

nikomatsakis (Mar 14 2019 at 20:33, on Zulip):

I see a few options

Albin Stjerna (Mar 14 2019 at 20:33, on Zulip):

agreed

nikomatsakis (Mar 14 2019 at 20:33, on Zulip):
nikomatsakis (Mar 14 2019 at 20:34, on Zulip):

but I think that's not the right thing to do

nikomatsakis (Mar 14 2019 at 20:34, on Zulip):

it feels a bit premature

Albin Stjerna (Mar 14 2019 at 20:34, on Zulip):

I think that's what we do after we have tried everything else

nikomatsakis (Mar 14 2019 at 20:34, on Zulip):

and I'm not super keen to make datafrog-opt more complex than it already is until we're sure we're happy

nikomatsakis (Mar 14 2019 at 20:34, on Zulip):

another option I see would be

nikomatsakis (Mar 14 2019 at 20:34, on Zulip):
nikomatsakis (Mar 14 2019 at 20:35, on Zulip):

so, right now, the polonius gets a set of input facts generated by rustc

Albin Stjerna (Mar 14 2019 at 20:35, on Zulip):

ah

nikomatsakis (Mar 14 2019 at 20:35, on Zulip):

these ones

nikomatsakis (Mar 14 2019 at 20:35, on Zulip):

but in some cases rustc has to do a fair amount of work to generate those facts,

nikomatsakis (Mar 14 2019 at 20:35, on Zulip):

and some of this work can/should be moved into polonius

Albin Stjerna (Mar 14 2019 at 20:36, on Zulip):

ah, and that work might be redundant with work later done by datafrog

Albin Stjerna (Mar 14 2019 at 20:36, on Zulip):

of course, because it also propagates constraints

Albin Stjerna (Mar 14 2019 at 20:36, on Zulip):

in fact, if I have understood things correctly, it only propagates and never searches/backtracks, right?

nikomatsakis (Mar 14 2019 at 20:36, on Zulip):

the goal I think would be that the set of facts is ultimately something we can read fairly directly from the MIR and type-check results

nikomatsakis (Mar 14 2019 at 20:36, on Zulip):

in fact, if I have understood things correctly, it only propagates and never searches/backtracks, right?

right, datalog does not require backtracking to solve

nikomatsakis (Mar 14 2019 at 20:37, on Zulip):

I believe the only fact that is presently computed via a very "datalog-y like analysis" is region_live_at

nikomatsakis (Mar 14 2019 at 20:37, on Zulip):

I guess hmm a simple thing we could start with

nikomatsakis (Mar 14 2019 at 20:38, on Zulip):

might be to modify rustc to generalize more basic liveness facts -- e.g., this variable is defined here, this variable is used there

nikomatsakis (Mar 14 2019 at 20:38, on Zulip):

and then we could write some datafrog code to compute liveness, even if we don't use it for anything

nikomatsakis (Mar 14 2019 at 20:38, on Zulip):

(Yet)

nikomatsakis (Mar 14 2019 at 20:38, on Zulip):

it's a first step towards the change I'm talking about, and it would definitely mean you understand all the parts

nikomatsakis (Mar 14 2019 at 20:39, on Zulip):

I think we'll need a few more bits of things after that to complete the change

nikomatsakis (Mar 14 2019 at 20:39, on Zulip):

(as it happens, the Lark compiler that I mentioned already does this)

nikomatsakis (Mar 14 2019 at 20:39, on Zulip):

if we did a video session tomorrow @Albin Stjerna we could walk through what will be required

nikomatsakis (Mar 14 2019 at 20:39, on Zulip):

I'll record it, post it to youtube, then you can look back over it ;)

Albin Stjerna (Mar 14 2019 at 20:40, on Zulip):

Always a good thing to have :)

Albin Stjerna (Mar 14 2019 at 20:40, on Zulip):

Ok, so would that calculation be done in Polonius and then fed back into rustc, or is it only needed for the borrowcheck?

nikomatsakis (Mar 14 2019 at 20:41, on Zulip):

the latter, it is only needed for borrow check

nikomatsakis (Mar 14 2019 at 20:41, on Zulip):

Hmm, would 14:00 Boston / 19:00 CET work for you?

Albin Stjerna (Mar 14 2019 at 20:41, on Zulip):

Ah, Ok, then I see why you would want to move it

nikomatsakis (Mar 14 2019 at 20:41, on Zulip):

I could maybe do earlier instead

nikomatsakis (Mar 14 2019 at 20:41, on Zulip):

Ok, so would that calculation be done in Polonius and then fed back into rustc, or is it only needed for the borrowcheck?

(actually some other parts of the compiler do similar calculations, but they do them somewhat differently)

nikomatsakis (Mar 14 2019 at 20:41, on Zulip):

Hmm, would 14:00 Boston / 19:00 CET work for you?

or we could do monday

nikomatsakis (Mar 14 2019 at 20:42, on Zulip):

say at 10:30 Boston / 15:30 CET or 11:00 Boston / 16:00 CET

nikomatsakis (Mar 14 2019 at 20:42, on Zulip):

I'd like to do it soon, so you can get started :)

nikomatsakis (Mar 14 2019 at 20:43, on Zulip):

but then maybe just starting out by trying to upgrade the version of polonius rustc uses / change that line will keep ya busy for one day ;)

Albin Stjerna (Mar 14 2019 at 20:43, on Zulip):

Yes, me too. I would prefer tomorrow to Monday, because I have a meeting at 15:00 CET (probably a short one)

nikomatsakis (Mar 14 2019 at 20:43, on Zulip):

ok, let's do tomorrow then. Does that time work? I could .. maybe also do 11:00 / 16:00 tomorrow.

Albin Stjerna (Mar 14 2019 at 20:43, on Zulip):

I think it would, but it doesn't hurt to pipeline a few things

nikomatsakis (Mar 14 2019 at 20:44, on Zulip):

(Also, if you're online, I might be able to do earlier, we could play it a bit by ear and I can ping you)

nikomatsakis (Mar 14 2019 at 20:44, on Zulip):

ok, let's do tomorrow then. Does that time work? I could .. maybe also do 11:00 / 16:00 tomorrow.

let's do this. That leaves my afternoon more free

Albin Stjerna (Mar 14 2019 at 20:44, on Zulip):

12:00 Boston would be perfect for me (I get off work at the library 16:00 CET), but anything goes after that really

nikomatsakis (Mar 14 2019 at 20:45, on Zulip):

Ah, ok, then never mind

nikomatsakis (Mar 14 2019 at 20:45, on Zulip):

I can't do 12:00 so let's do 14:00 / 19:00

Albin Stjerna (Mar 14 2019 at 20:46, on Zulip):

I would probably be home around 16:20 or so though

Albin Stjerna (Mar 14 2019 at 20:46, on Zulip):

If that works for you

nikomatsakis (Mar 14 2019 at 20:47, on Zulip):

hmm

nikomatsakis (Mar 14 2019 at 20:47, on Zulip):

I'm not sure how much time we'll need

nikomatsakis (Mar 14 2019 at 20:47, on Zulip):

I guess we could try it then, say for 30 minutes, that might suffice

nikomatsakis (Mar 14 2019 at 20:47, on Zulip):

and continu later

Albin Stjerna (Mar 14 2019 at 20:47, on Zulip):

Yes, which could even have the advantage of giving me some time to research things for a later session if we need one

nikomatsakis (Mar 14 2019 at 20:47, on Zulip):

er wait

nikomatsakis (Mar 14 2019 at 20:47, on Zulip):

I was doing math wrong

Albin Stjerna (Mar 14 2019 at 20:47, on Zulip):

...relate

nikomatsakis (Mar 14 2019 at 20:48, on Zulip):

well wait

nikomatsakis (Mar 14 2019 at 20:48, on Zulip):

no I wasn't

nikomatsakis (Mar 14 2019 at 20:48, on Zulip):

ok, perfect

nikomatsakis (Mar 14 2019 at 20:48, on Zulip):

we'll do 11:30 / 16:30

Albin Stjerna (Mar 14 2019 at 20:48, on Zulip):

Great!

nikomatsakis (Mar 14 2019 at 20:48, on Zulip):

ping me when you get back @Albin Stjerna and we can start a few minutes earlier :)

Albin Stjerna (Mar 14 2019 at 20:48, on Zulip):

Sure!

nikomatsakis (Mar 14 2019 at 20:48, on Zulip):

ok, very good. enough for 1 day?

Albin Stjerna (Mar 14 2019 at 20:48, on Zulip):

Yes, definitely!

nikomatsakis (Mar 14 2019 at 20:49, on Zulip):

ps @Matthew Jasper I'm assuming you have enough to do and are mostly watching along?

Matthew Jasper (Mar 14 2019 at 20:49, on Zulip):

Yes, I have enough to do with normal NLL

Albin Stjerna (Mar 14 2019 at 21:01, on Zulip):

Ok, but I guess that's it for the meeting? I don't think I have anything else

nikomatsakis (Mar 14 2019 at 21:13, on Zulip):

@Albin Stjerna oh, yes I think it is :)

Last update: Nov 15 2019 at 20:55UTC