Stream: t-compiler/wg-nll

Topic: polonius subset considered unnecessary


nikomatsakis (Nov 30 2018 at 15:51, on Zulip):

So, I've been thinking about the polonius rules. I .. am pretty sure that the transitive closure computation for subset is just plain unnecessary, if the main thing you are interested in is which loans are live at a particular point.

Interestingly, cloning the naive rules and removing the transitive closure for subset yields both a simple, readable specification, but also a faster one:

Algorithm Time for clap-rs LOC
Naive 31.73s 221
DatafrogOpt 3.929s 454
Reachable 2.360s 165
LocationInsensitive 0.646s 153
nikomatsakis (Nov 30 2018 at 15:51, on Zulip):

cc @lqd :point_up:

lqd (Nov 30 2018 at 15:52, on Zulip):

oh, nice

nikomatsakis (Nov 30 2018 at 15:52, on Zulip):

I think the reason I always wanted to keep the transitive closure computation for subset before was because we're going to need something like it in order to deal with errors around lifetime parameters.

nikomatsakis (Nov 30 2018 at 15:53, on Zulip):

But I think you can model those as special loans (which is basically what they are anyway)

nikomatsakis (Nov 30 2018 at 15:53, on Zulip):

I'm sort of annoying by all this though :P because I thought I had some great insight yesterday about a new rule to add that would "carry" requires relationships across cfg edges.

nikomatsakis (Nov 30 2018 at 15:53, on Zulip):

but it turns out my insight is mostly that some of my old rules were unnecessary :P

nikomatsakis (Nov 30 2018 at 15:53, on Zulip):

somehow doesn't feel as nice ;)

lqd (Nov 30 2018 at 15:54, on Zulip):

the result is good tho

lqd (Nov 30 2018 at 15:54, on Zulip):

did you by any chance run the rustc test suite with the Reachable variant ?

lqd (Nov 30 2018 at 15:59, on Zulip):

it's funny that this whole thing started with "optimizing the transitive closure" subject and we just needed to optimize it away :)

nikomatsakis (Nov 30 2018 at 16:05, on Zulip):

did you by any chance run the rustc test suite with the Reachable variant ?

not yet

nikomatsakis (Nov 30 2018 at 16:05, on Zulip):

I just build the latest master

lqd (Nov 30 2018 at 16:05, on Zulip):

model those as special loans
would this be in the polonius rules or in rustc's "lowering" to facts ?

nikomatsakis (Nov 30 2018 at 16:06, on Zulip):

probably polonius rules

nikomatsakis (Nov 30 2018 at 16:06, on Zulip):

in particular, it knows the set of universal regions

nikomatsakis (Nov 30 2018 at 16:06, on Zulip):

but I guess could be either

nikomatsakis (Nov 30 2018 at 16:06, on Zulip):

I'd sort of like push more and more into polonius eventually though

nikomatsakis (Nov 30 2018 at 16:06, on Zulip):

the tl;dr is that if you have some outlives relationships that ultimately require 'a: 'b

nikomatsakis (Nov 30 2018 at 16:06, on Zulip):

we need to know that and check that the user declared it

nikomatsakis (Nov 30 2018 at 16:06, on Zulip):

but what this is really saying in polonius terms

nikomatsakis (Nov 30 2018 at 16:07, on Zulip):

is that the set of loans in 'a had better be a subset of the set of loans in 'b

nikomatsakis (Nov 30 2018 at 16:07, on Zulip):

so if we say that there is some special loan La that is only in 'a

nikomatsakis (Nov 30 2018 at 16:07, on Zulip):

and we find that requires('b, La, P) for some point P...

nikomatsakis (Nov 30 2018 at 16:08, on Zulip):

...then the user must have declared that 'a: 'b or else it's an error

nikomatsakis (Nov 30 2018 at 16:08, on Zulip):

something like that, though it has to be extended to higher universes too, but the same principle applies

lqd (Nov 30 2018 at 16:08, on Zulip):

oh interesting yeah

lqd (Nov 30 2018 at 16:09, on Zulip):

just the fact that's possible to do without needing the TC is good in any case

nikomatsakis (Nov 30 2018 at 16:09, on Zulip):

basically we can encode the outlives relationships from the declaration as relations

nikomatsakis (Nov 30 2018 at 16:10, on Zulip):

and then search for errors like:

universal_region_error :-
  universal_region(Ra, La), // universal region Ra has associated loan Lb
  universal_region(Rb, _),
  requires(Rb, La, _P),
  !universal_region_subset_transitive(Ra, Rb).
lqd (Nov 30 2018 at 16:11, on Zulip):

(note that some of the rustc tests will fail in the polonius mode; when I completed the cfg compression around the beginning of october there were then 37 of those failing tests if I remember correctly)

nikomatsakis (Nov 30 2018 at 16:11, on Zulip):

ps, @lqd, note that in the new rules all the transitive computation is in the requires relation, so it's really quite simple to restrict it only to loans we care about.

nikomatsakis (Nov 30 2018 at 16:12, on Zulip):

i.e., if we compute the "maybe failing" loans using a first pass location insensitive analysis

nikomatsakis (Nov 30 2018 at 16:12, on Zulip):

yeah that's why I wanted to do a baseline run

nikomatsakis (Nov 30 2018 at 16:12, on Zulip):

I will try to get that going now

lqd (Nov 30 2018 at 16:12, on Zulip):

oh that's good for the possible location insensitive prepass

nikomatsakis (Nov 30 2018 at 16:12, on Zulip):

yep

nikomatsakis (Nov 30 2018 at 16:13, on Zulip):

which runs in 0.6s

nikomatsakis (Nov 30 2018 at 16:13, on Zulip):

so it still laps all the others ;)

lqd (Nov 30 2018 at 16:13, on Zulip):

I have it in 100ms

nikomatsakis (Nov 30 2018 at 16:13, on Zulip):

I haven't integrated your latest changes to datafrog yet

lqd (Nov 30 2018 at 16:13, on Zulip):

with the "leapfrog" join

nikomatsakis (Nov 30 2018 at 16:13, on Zulip):

though I have them on a branch

nikomatsakis (Nov 30 2018 at 16:13, on Zulip):

I have to go lookup the cargo syntax for dealing with that

nikomatsakis (Nov 30 2018 at 16:14, on Zulip):

I guess I could just rewrite the toml to a path dependency

lqd (Nov 30 2018 at 16:14, on Zulip):

replace/patch ?

nikomatsakis (Nov 30 2018 at 16:14, on Zulip):

that feels so dirty

nikomatsakis (Nov 30 2018 at 16:14, on Zulip):

right

nikomatsakis (Nov 30 2018 at 16:14, on Zulip):

I just remember there are two ways to do it and I can never figure out why there are 2

nikomatsakis (Nov 30 2018 at 16:14, on Zulip):

does one of them not require me to edit the actual Cargo.toml?

nikomatsakis (Nov 30 2018 at 16:14, on Zulip):

that feels like the right one :)

nikomatsakis (Nov 30 2018 at 16:15, on Zulip):

also, I am...mostly happy since switching to DuckDuckGo, but dang does it suck at searches with the word "cargo" in them

lqd (Nov 30 2018 at 16:15, on Zulip):

I don't think we can avoid editing cargo.toml can we ?

nikomatsakis (Nov 30 2018 at 16:15, on Zulip):

apparently it really helps to know who I am for that :P

nikomatsakis (Nov 30 2018 at 16:15, on Zulip):

I don't think we can avoid editing cargo.toml can we ?

it feels like you should be able...

nikomatsakis (Nov 30 2018 at 16:15, on Zulip):

anyway not germane :)

nikomatsakis (Nov 30 2018 at 16:15, on Zulip):

I'd like to be able to do tests like this without having files git considers dirty in my repo :P

lqd (Nov 30 2018 at 16:16, on Zulip):

the :frog: changes would also allow to reopen/redo the "specialization" datafrog PR removing some allocations

lqd (Nov 30 2018 at 16:16, on Zulip):

and ofc changing the variants to use the join

lqd (Nov 30 2018 at 16:17, on Zulip):

although I think there's something I need to work out (or with Frank), possibly a bug/misunderstanding in the join, which would allow to remove more temporary indices

lqd (Nov 30 2018 at 16:18, on Zulip):

(no big deal, it's some uncommon cases, like where the regular join should have the same behaviour, although being able to work on Relations over Variables would allow these indices to be removed)

nikomatsakis (Nov 30 2018 at 16:19, on Zulip):

I actually can't find any docs for [replace] etc in https://doc.rust-lang.org/cargo/reference/

lqd (Nov 30 2018 at 16:19, on Zulip):

yeah it's patch IIRC

nikomatsakis (Nov 30 2018 at 16:19, on Zulip):

ah, found it

nikomatsakis (Nov 30 2018 at 16:19, on Zulip):

https://doc.rust-lang.org/cargo/reference/source-replacement.html

lqd (Nov 30 2018 at 16:19, on Zulip):

oh but also replace wow

lqd (Nov 30 2018 at 16:20, on Zulip):

at least it's documented yay

nikomatsakis (Nov 30 2018 at 16:20, on Zulip):

@lqd so when I use your branch

nikomatsakis (Nov 30 2018 at 16:20, on Zulip):

do I also have to edit the source?

lqd (Nov 30 2018 at 16:20, on Zulip):

yeah

nikomatsakis (Nov 30 2018 at 16:20, on Zulip):

or will from_join and friends use it automatically

lqd (Nov 30 2018 at 16:21, on Zulip):

it's a completely different api unfortunately

nikomatsakis (Nov 30 2018 at 16:21, on Zulip):

oh

nikomatsakis (Nov 30 2018 at 16:21, on Zulip):

:)

lqd (Nov 30 2018 at 16:21, on Zulip):

I'll try to get you one of the variants using it

nikomatsakis (Nov 30 2018 at 16:21, on Zulip):

well hold up

nikomatsakis (Nov 30 2018 at 16:21, on Zulip):

I'll open a PR with my changes I guess

nikomatsakis (Nov 30 2018 at 16:21, on Zulip):

then you can port that ;)

lqd (Nov 30 2018 at 16:22, on Zulip):

lol

nikomatsakis (Nov 30 2018 at 16:22, on Zulip):

well

nikomatsakis (Nov 30 2018 at 16:22, on Zulip):

if you have a link ready

nikomatsakis (Nov 30 2018 at 16:22, on Zulip):

that's fine too

lqd (Nov 30 2018 at 16:22, on Zulip):

I can take care of it

lqd (Nov 30 2018 at 16:23, on Zulip):

but here's an example of the location_insensitive variant using the treefrog join just to show you how different it is

lqd (Nov 30 2018 at 16:24, on Zulip):

I guess Frank's post also shows some, but I'll port Reachable and push the other 2 I've already done then

lqd (Nov 30 2018 at 16:26, on Zulip):

(unrelated: about the switch to "beta" -- since you're removing try do we still need the tests returning a Result<(), Error> ?)

nikomatsakis (Nov 30 2018 at 16:28, on Zulip):

PS I updated my table with LOC just for fun:

Algorithm Time for clap-rs LOC
Naive 31.73s 221
DatafrogOpt 3.929s 454
Reachable 2.360s 165
LocationInsensitive 0.646s 153
nikomatsakis (Nov 30 2018 at 16:28, on Zulip):

(unrelated: about the switch to "beta" -- since you're removing try do we still need the tests returning a Result<(), Error> ?)

ah, I ... guess not? depends if they are using ? I guess?

lqd (Nov 30 2018 at 16:30, on Zulip):

Reachable is going to be short and sweet :)

lqd (Nov 30 2018 at 16:30, on Zulip):

(ok I'll comment on the rustfmt PR -- or meh actually, no big deal, we can have an ? instead of an .expect() :)

nikomatsakis (Nov 30 2018 at 16:32, on Zulip):

I'm gonna merge https://github.com/rust-lang-nursery/polonius/pull/85

nikomatsakis (Nov 30 2018 at 16:32, on Zulip):

I've decided it's worth avoiding nightly dependencies in stuff the compiler uses if at all possible

nikomatsakis (Nov 30 2018 at 16:32, on Zulip):

even if not strictly necessary

lqd (Nov 30 2018 at 16:33, on Zulip):

do you want to switch to stable on dec 6 ?

nikomatsakis (Nov 30 2018 at 16:49, on Zulip):

ideally, but beta suffices

nikomatsakis (Nov 30 2018 at 16:49, on Zulip):

since the compiler builds on beta :)

lqd (Nov 30 2018 at 16:56, on Zulip):

sure :)

lqd (Nov 30 2018 at 16:57, on Zulip):

(I wonder how would CFG compression behave over the Reachable variant)

lqd (Nov 30 2018 at 17:20, on Zulip):

(oh I forgot, in my CFG compression PR, there's also the dataset from the rustc "polonius smoke test"; it's an interesting one because IIRC it also contained functions which shouldn't compile, & important to have as we currently mostly test loans and not errors yet)

Matthew Jasper (Nov 30 2018 at 18:17, on Zulip):

Maybe I'm missing something, how does this work without TC?

fn f(x: &mut &i32) {
    let y = x;
    *y = &g(); // how does this loan end up having to outlive the function?
}
nikomatsakis (Nov 30 2018 at 18:27, on Zulip):

let me check because I may be missing something :)

nikomatsakis (Nov 30 2018 at 18:29, on Zulip):

(that is, maybe that's the piece I was missing; I remember doing many rounds in the original polonius days with various examples of how info had to travel)

nikomatsakis (Nov 30 2018 at 18:30, on Zulip):

(and I was planning on reproducing those rounds as part of a write-up :)

nikomatsakis (Nov 30 2018 at 18:31, on Zulip):

before that:

./x.py test src/test/ui --compare-mode polonius --bless

gives me

FAILED. 177 passed; 17 failed; 4847 ignored; 0 measured; 0 filtered out
nikomatsakis (Nov 30 2018 at 18:33, on Zulip):

@Matthew Jasper but yeah you may be right :) maybe this is a false insight =)

nikomatsakis (Nov 30 2018 at 18:34, on Zulip):

I guess that those 17 failures are not including my fixes though

RalfJ (Nov 30 2018 at 20:03, on Zulip):

but it turns out my insight is mostly that some of my old rules were unnecessary :P

IMO those are amongst the best insights :D

nikomatsakis (Nov 30 2018 at 20:16, on Zulip):

except when maybe it is wrong...I have to think a bit more, but I think I may have just forgotten about an important part of how polonius works (which @Matthew Jasper reminded me of :P)

nikomatsakis (Nov 30 2018 at 20:16, on Zulip):

but right now i'm trying to do reviews :)

lqd (Nov 30 2018 at 21:53, on Zulip):

/me still on the edge of my seat :p

Last update: Nov 21 2019 at 23:50UTC