Stream: t-compiler/wg-polonius

Topic: names of atoms


nikomatsakis (Sep 13 2019 at 20:16, on Zulip):

OK I couldn't help myself. I took a stab at creating names for each of the atoms in polonius#124. Thoughts?

nikomatsakis (Sep 13 2019 at 20:17, on Zulip):
nikomatsakis (Sep 13 2019 at 20:17, on Zulip):

Note that the first letters are all unique, though I think we should indeed prefer to use full words when we can :)

lqd (Sep 13 2019 at 20:17, on Zulip):

points -> nodes to free up P/Paths ? :)

nikomatsakis (Sep 13 2019 at 20:17, on Zulip):

Yes :P

lqd (Sep 13 2019 at 20:17, on Zulip):

:)

nikomatsakis (Sep 13 2019 at 20:18, on Zulip):

but also, well, I can't remember why, but I remember thinking that Point felt a bit ambiguous in the past

nikomatsakis (Sep 13 2019 at 20:18, on Zulip):

it may have just been the letter "P" really

nikomatsakis (Sep 13 2019 at 20:18, on Zulip):

but it feels like saying "points are the nodes in the control-flow graph" feels silly

nikomatsakis (Sep 13 2019 at 20:18, on Zulip):

like, node is the standard term...

lqd (Sep 13 2019 at 20:18, on Zulip):

true

nikomatsakis (Sep 13 2019 at 20:18, on Zulip):

(...though point is also fairly widely used)

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

it's pretty nice overall

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

I'm feeling pretty good about origin right now though.

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

provenance just feels kind of jargon-y to me?

nikomatsakis (Sep 13 2019 at 20:20, on Zulip):

but that's the main one I'm debating about ;)

lqd (Sep 13 2019 at 20:20, on Zulip):

:) I guess it is yeah, and origin seems more approachable

nikomatsakis (Sep 13 2019 at 20:22, on Zulip):

also it's easier to type

lqd (Sep 13 2019 at 20:23, on Zulip):

provenance feels good in oxide

lqd (Sep 13 2019 at 20:24, on Zulip):

at least they won't share the name if the models end up slightly different, that could be confusing

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

I also like origin, I frequently ran into the problem of talking about "provenance variables of variables"

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

Origin helps a lot here

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

(also, dropping "variable" after provenance of course)

lqd (Sep 15 2019 at 19:59, on Zulip):

alright let's do this then

lqd (Sep 15 2019 at 22:42, on Zulip):

next we can improve the names of the relations as well :)

lqd (Sep 16 2019 at 10:46, on Zulip):

should I switch the atoms in this doc to the new names ? BTW I think it's ready-ish for review, how do we want to proceed with this: open a PR or iterate on hackmd until ready ?

lqd (Sep 16 2019 at 21:07, on Zulip):

In the last meeting I thought we used single-letters for generic types a lot, but we actually only did it once. They are now words in this new PR along with converting most of the region uses to origin (except for the variable names in datafrog join closures and the datalog rules comments, which I didn't want to touch just yet). I also didn't change the other two atoms (maybe we don't really need to change Point :thinking:, anyway)

Albin Stjerna (Sep 17 2019 at 07:57, on Zulip):

Looks good! I'm getting the impression I should...wait with any changes to Polonius :)

Albin Stjerna (Sep 17 2019 at 07:58, on Zulip):

This suits me perfectly anyway, as I'm swamped with the courses I'm TA:ing and finishing up my thesis and presentation

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

should I switch the atoms in this doc to the new names ? BTW I think it's ready-ish for review, how do we want to proceed with this: open a PR or iterate on hackmd until ready ?

new names!

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

will do, and then open a PR about the inputs I know (pre-liveness) and Albin can then open a PR about the facts they know if that's ok ?

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

sounds good

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

I'll do so later tonight

lqd (Sep 17 2019 at 20:09, on Zulip):

PR posted here — I'm unsure about a couple places wrt universal regions naming, and about the whole thing in general :)

lqd (Sep 18 2019 at 10:20, on Zulip):

I'm trying out this in the variant's comments to describe the rules

// subset(origin1, origin3, point) :-
//  subset(origin1, origin2, point),
//  subset(origin2, origin3, point).

and I kinda like the a e s t h e t i c s tbh, but the lowercasedness might trip up some datalog engines, would you rather have a leading uppercase letter ? but since we're not likely to copy paste the rules out of the various bits of the code, and rather have the rules documented in a single place in the book, maybe this isn't a problem for you @nikomatsakis ?

lqd (Sep 18 2019 at 10:28, on Zulip):

in the same vein, I don't expect us to .decl the relations in the variants' comments even if we used the soufflé format in the book

lqd (Sep 18 2019 at 11:51, on Zulip):

The Great Renaming ™ step 2 has advanced, and here is how the Naive variant would look. Note that I haven't done the renaming of Points to Nodes as I'd like to try using the word "point" everywhere at first and see how that looks like. Elsewhere in this branch, almost everything has been renamed (so, except the CFG as I said, there will be still ps and qs but that should mostly be it for the single-letters) but the init/liveness (in case it would conflict too much with WIP work from Albin). What does everyone think, is that better ?

lqd (Sep 18 2019 at 17:37, on Zulip):

(and this is how the Naive variant looks using names for points, thoughts ?)

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

I think I would prefer Origin1, versus all lower-case. I think it's useful to be able to identify variables.

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

I guess I'd also like to be able to copy-and-paste with minimal fuss.

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

sure, I'll do that then :)

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

oh hmm

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

I guess the lower case names in the comments match the source variables?

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

that seems valuable

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

I think that's fine

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

I was thinking more about "the book"

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

it's interesting

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

maybe we can try like that last link for a while, and see how it feels ?

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

or I can do the title casing now, it's nbd

lqd (Sep 18 2019 at 20:00, on Zulip):

for the book itself we agree it'd be better for the rules to be usable in a datalog engine with minimal work

lqd (Sep 18 2019 at 20:48, on Zulip):

(since we'll be using real words, maybe I can switch from the verbose-ish "True if the restrictions of the loan loan need to be enforced at the point point" to the equally-clear "True if the restrictions of the loan need to be enforced at the point")

Tshepang Lekhonkhobe (Sep 19 2019 at 04:51, on Zulip):

OK I couldn't help myself. I took a stab at creating names for each of the atoms in polonius#124. Thoughts?

should we not prefer bindings, given that variables can refer to values that do not change

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

(I feel variable is pretty standard terminology, myself -- also, these do not necessarily correspond to bindings in the rust language)

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

(I feel variable is pretty standard terminology, myself -- also, these do not necessarily correspond to bindings in the rust language)

Speaking of this, is there a more comprehensive guide to MIR somewhere than in the compiler book? For example, I am not at all sure about how MIR variables correspond to Rust variables

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

nope but it'd be good to accumulate questions you've had in a rustc-guide issue

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

well I mean there is the RFC etc

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

which maybe clarifies some of that

nikomatsakis (Oct 03 2019 at 09:39, on Zulip):

PS, I'm finding that working on these RBR slides is a good way to "test out" these atom names

lqd (Oct 03 2019 at 09:40, on Zulip):

how do they feel ?

nikomatsakis (Oct 03 2019 at 09:42, on Zulip):

Mostly good.

nikomatsakis (Oct 03 2019 at 09:42, on Zulip):

I was just now struggling a bit around the word origin

lqd (Oct 03 2019 at 09:42, on Zulip):

haha :)

nikomatsakis (Oct 03 2019 at 09:43, on Zulip):

I wanted to talk about how, whenever a variable is live, any origins that appear in its type must be live .. ah, maybe that's actually the mistake

nikomatsakis (Oct 03 2019 at 09:43, on Zulip):

what I am really trying to say is that

nikomatsakis (Oct 03 2019 at 09:43, on Zulip):

the loans that appear in its type are live

nikomatsakis (Oct 03 2019 at 09:43, on Zulip):

i.e., the problem is focusing on the "origins" at all

nikomatsakis (Oct 03 2019 at 09:44, on Zulip):

(also, it's not clear that "provenance" would have helped -- and lifetime can be downright confusing)

nikomatsakis (Oct 03 2019 at 09:44, on Zulip):

put another way, I sometimes want to be sloppy and talk about (e.g.) the "origin of a variable"

nikomatsakis (Oct 03 2019 at 09:44, on Zulip):

and that felt confusing to me

nikomatsakis (Oct 03 2019 at 09:44, on Zulip):

but really I think the flaw is that being sloppy like that is just kind of ungreat

lqd (Oct 03 2019 at 09:44, on Zulip):

would the "region of a variable" have been clearer, say ?

nikomatsakis (Oct 03 2019 at 09:44, on Zulip):

not really

nikomatsakis (Oct 03 2019 at 09:45, on Zulip):

that's kind of what I mean

nikomatsakis (Oct 03 2019 at 09:45, on Zulip):

it's confusing no matter which word you use, istm

lqd (Oct 03 2019 at 09:45, on Zulip):

that's kind of the reason why (re)naming them was hard as well

nikomatsakis (Oct 03 2019 at 09:45, on Zulip):

but the "loans that appear in the variable's type", while wordy, seems reasonable to explain

lqd (Oct 03 2019 at 09:46, on Zulip):

the loans are key

Albin Stjerna (Oct 07 2019 at 08:56, on Zulip):

but the "loans that appear in the variable's type", while wordy, seems reasonable to explain

I had similar problems in my thesis presentation and I think this is probably the best way to resolve them

Albin Stjerna (Oct 07 2019 at 08:56, on Zulip):

I mean, the origins are just placeholders anyway?

Albin Stjerna (Oct 07 2019 at 08:57, on Zulip):

Basically, what I did was hand-wave and say "these relations come into contact in order to figure out which of these loans are live, and when a live loan is violated we have an error"

Albin Stjerna (Oct 07 2019 at 08:58, on Zulip):

by which I mean I literally waved my hands across a chart showing the flow between the different relations

Last update: Nov 15 2019 at 20:05UTC