Stream: t-compiler/wg-polonius

Topic: discussing Polonius design


nikomatsakis (Feb 15 2019 at 14:25, on Zulip):

So we had planned to do a Polonius design walk through (cc @lqd, but I forget who else) -- I'd like to schedule that for next week.

RalfJ (Feb 15 2019 at 14:27, on Zulip):

if the timing works out I'd also be interested

Aaron Weiss (Feb 15 2019 at 14:31, on Zulip):

Next week should work for me, depending on time.

nikomatsakis (Feb 15 2019 at 14:45, on Zulip):

I should create a WG-polonius alias, shouldn't I

csmoe (Feb 15 2019 at 14:47, on Zulip):

+1

Cem Karan (Feb 15 2019 at 14:55, on Zulip):

@nikomatsakis Is this walk through intended to be like the compiler lecture series you have going?

Santiago Pastorino (Feb 15 2019 at 15:29, on Zulip):

@nikomatsakis :+1:

nikomatsakis (Feb 15 2019 at 16:09, on Zulip):

@Cem Karan "like" in what sense?

nikomatsakis (Feb 15 2019 at 16:09, on Zulip):

I was probably shooting for something like the Salsa video where I discussed with @Jonathan Turner

nikomatsakis (Feb 15 2019 at 16:10, on Zulip):

I'm not sure yet whether "all" these things are part of compiler lecture series or if that should be a subset, aiming at a wider audience

nikomatsakis (Feb 15 2019 at 16:10, on Zulip):

cc @Albin Stjerna also

nikomatsakis (Feb 15 2019 at 16:10, on Zulip):

Anyway, I'm thinking I'll create a doodle poll for Tuesday to try and find a good time?

Cem Karan (Feb 15 2019 at 16:12, on Zulip):

@nikomatsakis In the sense of being for a wider audience/people who are not familiar with Polonius at all. Basically, I'm wondering if this the undergraduate intro, or the PhD student "intro"...

nikomatsakis (Feb 15 2019 at 16:20, on Zulip):

OK -- here is a doodle poll. I just put the whole day though I think that I personally may only be available in (my) afternoon)

nikomatsakis (Feb 15 2019 at 16:21, on Zulip):

so really there may be far fewer actionable choices ;)

nikomatsakis (Feb 15 2019 at 16:21, on Zulip):

@Cem Karan I think the answer is that I plan to target this at people familiar-ish with Rust and the borrowing rules, but not necessarily PhD students :)

nikomatsakis (Feb 15 2019 at 16:21, on Zulip):

So maybe somewhere in between

Cem Karan (Feb 15 2019 at 16:43, on Zulip):

@nikomatsakis OK, in that case, I'll take as much as I can from the conversation. Still desperately trying to learn everything I can about rust! :)

nikomatsakis (Feb 15 2019 at 17:01, on Zulip):

@Cem Karan Great! I'd definitely like to have people from a variety of skill levels, to help ensure the material is comprehensible.

nikomatsakis (Feb 19 2019 at 18:46, on Zulip):

Hey all! So I'm planning to do this call today, as scheduled.

nikomatsakis (Feb 19 2019 at 18:47, on Zulip):

I've got a paper document that kind of contains my "lesson plan", though as part of the call I expect to create a fresh doc and kind of walk through it bit by bit.

nikomatsakis (Feb 19 2019 at 18:47, on Zulip):

My hope is that y'all will ask me lots of questions to make up for my lack of preparation time :)

nikomatsakis (Feb 19 2019 at 18:48, on Zulip):

cc @Cem Karan @Aaron Weiss @Santiago Pastorino @Albin Stjerna @lqd @Matthew Jasper @Keith Yeung and not sure who else =)

nikomatsakis (Feb 19 2019 at 18:48, on Zulip):

Recorded call where we interactively explore some of the key examples that inform the Polonius design.

Join Zoom Meeting
https://zoom.us/j/991477503

One tap mobile
+19294362866,,991477503# US
+16699006833,,991477503# US (San Jose)

Dial by your location
+1 929 436 2866 US
+1 669 900 6833 US (San Jose)
Meeting ID: 991 477 503
Find your local number: https://zoom.us/u/aUzQdVyqy

nikomatsakis (Feb 19 2019 at 18:48, on Zulip):

I am sort of expecting we may have to do another call to get to some of the more complex stuff

Cem Karan (Feb 19 2019 at 18:49, on Zulip):

Sounds good to me! I may cut in and out, my zoom client is acting flaky again.

nikomatsakis (Feb 19 2019 at 18:49, on Zulip):

Dropbox paper document that we'll create during the call is here.

nikomatsakis (Feb 19 2019 at 18:51, on Zulip):

cc @Zarenor

Zarenor (Feb 19 2019 at 18:53, on Zulip):

Thanks for pinging me. I'll definitely be listening in - I'll try to contribute a question or two, but my schedule has gotten a little busier than I'd like.

Aaron Weiss (Feb 19 2019 at 18:56, on Zulip):

@nikomatsakis is the meeting actually open already? It's just telling me "meeting has not started."

Albin Stjerna (Feb 19 2019 at 19:00, on Zulip):

Sounds good to me! I may cut in and out, my zoom client is acting flaky again.

I couldn't even install it on my machine; the installer crashed, so I'm using the Web client

Cem Karan (Feb 19 2019 at 19:01, on Zulip):

@Albin Stjerna The only way I've ever gotten zoom to work is in a virtual machine, and even then I have to phone in to get audio. If you can spin up a virtual box image fast enough, it might work for you...

nikomatsakis (Feb 19 2019 at 19:02, on Zulip):

@Aaron Weiss should have started now

nikomatsakis (Feb 19 2019 at 19:02, on Zulip):

can you all hear me?

nikomatsakis (Feb 19 2019 at 19:02, on Zulip):

I don't hear anyone else :)

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

you might have to enable computer audio

Aaron Weiss (Feb 19 2019 at 19:03, on Zulip):

We can hear each other, including you.

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

can you all hear me?

I don't hear /anything/, but I think that's a problem on my end.

nikomatsakis (Feb 19 2019 at 19:07, on Zulip):

@Albin Stjerna any lukc?

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

@Albin Stjerna any lukc?

Nope, everything else works fine audo-wise, but not Zoom, in any browser.

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

Ok, now I have stuttering and weird audio and I guess that's good enough for now

nikomatsakis (Feb 19 2019 at 19:59, on Zulip):

@Albin Stjerna seems like you got it working

nikomatsakis (Feb 19 2019 at 19:59, on Zulip):

I hope?

nikomatsakis (Feb 19 2019 at 19:59, on Zulip):

I'll post that video at some point in near future

Albin Stjerna (Feb 19 2019 at 20:00, on Zulip):

@nikomatsakis Yep! I managed to get it installed via Homebrew, and that one worked great

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

thanks for the great presentation :)

nikomatsakis (Feb 19 2019 at 20:00, on Zulip):

I would certainly welcome feedback on points that were confusing (valid answers include "everything")

Albin Stjerna (Feb 19 2019 at 20:00, on Zulip):

Yes, thanks!

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

Aaron's question about loans vs regions was an interesting point

nikomatsakis (Feb 19 2019 at 20:00, on Zulip):

(Also, question for y'all -- could you see the notifications that were popping up on my screen)

nikomatsakis (Feb 19 2019 at 20:00, on Zulip):

hopefully not

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

yeah we could

nikomatsakis (Feb 19 2019 at 20:01, on Zulip):

oh .. dear

Albin Stjerna (Feb 19 2019 at 20:01, on Zulip):

Yes, at least near the end

nikomatsakis (Feb 19 2019 at 20:01, on Zulip):

ok, annoying

nikomatsakis (Feb 19 2019 at 20:01, on Zulip):

I wasn't sharing the whole screen, but I guess those were somehow considered part of the video

nikomatsakis (Feb 19 2019 at 20:01, on Zulip):

I'll try to edit them out :)

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

probably some creative use of cropping would be enough

nikomatsakis (Feb 19 2019 at 20:01, on Zulip):

yeah

nikomatsakis (Feb 19 2019 at 20:01, on Zulip):

mostly I want to be sure not to miss any

nikomatsakis (Feb 19 2019 at 20:02, on Zulip):

apparently I did not disable notifications correctly

nikomatsakis (Feb 19 2019 at 20:02, on Zulip):

ok, apparently "do not disturb" is called "focus assist" on Windows

lqd (Feb 19 2019 at 20:03, on Zulip):

oh someone mentioned it in zoom chat

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

Also, sorry for yawning so much near the end, it's because I've had a long day and it's night here, not because I was bored :)

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

(if anyone was watching my video feed)

nikomatsakis (Feb 19 2019 at 20:07, on Zulip):

oh someone mentioned it in zoom chat

oh well, I missed that

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

now we'll know the lingo

Albin Stjerna (Feb 19 2019 at 20:08, on Zulip):

Yes, and I know that I have to un-learn some constraint programming lingo using the same overloaded terms

Albin Stjerna (Feb 19 2019 at 20:10, on Zulip):

I'm still a bit fuzzy on where the project is currently, though. The repo you showed us is the prototype, but what is missing from it?

nikomatsakis (Feb 19 2019 at 20:10, on Zulip):

@Albin Stjerna good question, good topic to dig into more for next time :)

nikomatsakis (Feb 19 2019 at 20:11, on Zulip):

the prototype is "complete" in some sense

nikomatsakis (Feb 19 2019 at 20:11, on Zulip):

but I want to move more of the logic into it

nikomatsakis (Feb 19 2019 at 20:11, on Zulip):

right now it covers only the "core borrow checker" errors

nikomatsakis (Feb 19 2019 at 20:11, on Zulip):

but there are other sorts of errors it could be detecting

nikomatsakis (Feb 19 2019 at 20:12, on Zulip):

I'm not 100% sure which is the priority of things to attack, in my mind

Albin Stjerna (Feb 19 2019 at 20:12, on Zulip):

Ah, ok, and that would require some more prototyping I guess

nikomatsakis (Feb 19 2019 at 20:12, on Zulip):

i.e., I think there is good work to be done extending the current system to cover more stuff, but also I'd like to be validating the performance against real-world test cases and decidiing if we're going to need to do clever stuff

lqd (Feb 19 2019 at 20:12, on Zulip):

the most recent of Niko's posts about Polonius we haven't fully implemented yet (one is partially done, and one not at all)

Albin Stjerna (Feb 19 2019 at 20:13, on Zulip):

Ok so the next steps would be both prototyping and benchmarking then I guess, including benchmark selection?

lqd (Feb 19 2019 at 20:15, on Zulip):

"next" being the most important word ? :) those steps are needed for sure

lqd (Feb 19 2019 at 20:16, on Zulip):

(the order/priorities are still unclear as of now I think)

nikomatsakis (Feb 19 2019 at 20:17, on Zulip):

benchmarking to some extent we have

nikomatsakis (Feb 19 2019 at 20:17, on Zulip):

@Albin Stjerna btw I know you are traveling for a bit

Albin Stjerna (Feb 19 2019 at 20:17, on Zulip):

Ah, ok, that's the things at perf.rust-lang.org?

nikomatsakis (Feb 19 2019 at 20:17, on Zulip):

when do you expect to be back on line?

lqd (Feb 19 2019 at 20:19, on Zulip):

yeah perf.rlo is for rustc benchmarking (with some NLL specific info, but not polonius) and we can use that to benchmark specific builds for polonius as well; we also "track" it locally in the polonius repo itself, but mostly informally when doing PRs and such, at this moment

lqd (Feb 19 2019 at 20:19, on Zulip):

same for datafrog

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

@nikomatsakis Good question, I'm leaving tomorrow morning very early and probably have intermittent connectivity during my travel. I land Thursday around 9 am CEST, but I don't think I'll get anything done before Friday.

Albin Stjerna (Feb 19 2019 at 20:22, on Zulip):

@lqd Ok, and is the idea to use datafrog in the final version as well, i.e. is the plan to optimise and improve it along with polonius?

lqd (Feb 19 2019 at 20:22, on Zulip):

AFAICT it is the plan now

lqd (Feb 19 2019 at 20:24, on Zulip):

contributors, Frank, etc have done so in the past for example (improving datafrog "for" polonius)

lqd (Feb 19 2019 at 20:25, on Zulip):

but as you saw during the meeting, other datalog engines could be similarly used I assume

lqd (Feb 19 2019 at 20:26, on Zulip):

probably because of performance reasons, which ties into your other benchmarkings points

Aaron Weiss (Feb 19 2019 at 20:26, on Zulip):

Aaron's question about loans vs regions was an interesting point

@lqd glad to hear it since from my perspective, it was pretty specific (i.e. it's more-or-less "is there a reason you're doing something different than I'm doing that I haven't realized?") :sweat_smile:

lqd (Feb 19 2019 at 20:27, on Zulip):

it seems fast for now, but we don't have many datapoints :)

lqd (Feb 19 2019 at 20:28, on Zulip):

@Aaron Weiss it didn't come off as dismissive or anything I feel :)

Aaron Weiss (Feb 19 2019 at 20:28, on Zulip):

I was more worried that Niko knew something I didn't know yet about why the current approach is necessary!

lqd (Feb 19 2019 at 20:28, on Zulip):

oh

Albin Stjerna (Feb 19 2019 at 20:29, on Zulip):

I have some connections to constraint programming people, including the people at Monash I will be visiting, including some Prolog people, so maybe I can at least score some tricky benchmarks and/or smart data structures and algorithms

Albin Stjerna (Feb 19 2019 at 20:29, on Zulip):

But I know absolutely nothing about Datalog

Aaron Weiss (Feb 19 2019 at 20:29, on Zulip):

It seems like the answer is that both ways can probably work though, which is good.

lqd (Feb 19 2019 at 20:30, on Zulip):

I myself don't know/remember if it was indeed absolutely necessary, I was assuming it was related to live loans, and possibly higher order regions and the likes, maybe diagnostics were involved so that's why I thought it was interesting :)

Aaron Weiss (Feb 19 2019 at 20:33, on Zulip):

The Oxide analogue I was thinking about is as follows: our borrow expressions are essentially &L0 x which we give the type &{ L0 -> x } T and then we directly update these region collections as we type check.

lqd (Feb 19 2019 at 20:33, on Zulip):

(and if indeed both ways do work, do they have different performance characteristics)

Aaron Weiss (Feb 19 2019 at 20:34, on Zulip):

It's interesting because some of the stuff that I imagine required some thought for Polonius (e.g. not propagating facts from dead regions) sort of fall out "automatically" from the way we're doing things.

lqd (Feb 19 2019 at 20:35, on Zulip):

yeah interesting

Aaron Weiss (Feb 19 2019 at 20:35, on Zulip):

On the other hand, naively implementing the Oxide type system would be painfully slow because at every move, borrow, and assignment, you need to look at the whole context to prove that the use is safe.

Aaron Weiss (Feb 19 2019 at 20:36, on Zulip):

So, what you'd want to actually do instead is some kind of caching of these facts, which seems to be equivalent to saying "do Polonius." :big_smile:

lqd (Feb 19 2019 at 20:41, on Zulip):

propagating through the CFG is tough for some of the bigger ones (which we have benchmarks of) so having a more "specialized representation" is an interesting possibility, but until we know more of the different analyses to do in polonius, vs say rustc, including diagnostics, liveness, etc it's still a bit up in the air

Keith Yeung (Feb 19 2019 at 23:12, on Zulip):

was the meetup recorded? I wasn't able to make it

nikomatsakis (Feb 19 2019 at 23:20, on Zulip):

yep but I have to edit/post the video

nikomatsakis (Feb 19 2019 at 23:20, on Zulip):

will do so in next day or two

nikomatsakis (Feb 19 2019 at 23:20, on Zulip):

I'm still working through my windows video pipeline :)

Last update: Nov 15 2019 at 20:00UTC