Stream: t-compiler/wg-nll

Topic: leapfrog


nikomatsakis (Dec 05 2018 at 12:00, on Zulip):

btw @lqd I've got a local build using leapfrog triejoin etc

lqd (Dec 05 2018 at 12:02, on Zulip):

oh you've switched the variants to this new API already ? I had PRs on the way so that people wouldn't have to bother

nikomatsakis (Dec 05 2018 at 12:04, on Zulip):

I switched to the new API; I'm not sure how you can avoid having to bother...?

nikomatsakis (Dec 05 2018 at 12:05, on Zulip):

(forked to a new topic)

nikomatsakis (Dec 05 2018 at 12:11, on Zulip):

this @lqd is the work I had done https://github.com/rust-lang-nursery/polonius/pull/88

lqd (Dec 05 2018 at 12:12, on Zulip):

one can't avoid having to bother, you didn't have to as I had already done it :)

nikomatsakis (Dec 05 2018 at 12:12, on Zulip):

oh I see :)

nikomatsakis (Dec 05 2018 at 12:12, on Zulip):

well, it was good for me anyway to better understand :)

lqd (Dec 05 2018 at 12:13, on Zulip):

sure sure :)

nikomatsakis (Dec 05 2018 at 12:13, on Zulip):

I'd be curious @lqd to get your 2 eurocents on these docs, too

nikomatsakis (Dec 05 2018 at 12:13, on Zulip):

in particular if that sounds like an accurate summary

nikomatsakis (Dec 05 2018 at 12:14, on Zulip):

though obviously for real end-users to understand it needs a few examples

lqd (Dec 05 2018 at 12:15, on Zulip):

I will look the 2 PRs over for sure at lunchbreak (in particular I feel like there were more possible uses of leapjoin in datafrog opt but I might be misremembering)

lqd (Dec 05 2018 at 12:16, on Zulip):

also "your 2 eurocents" = :smiley:

nikomatsakis (Dec 05 2018 at 12:16, on Zulip):

I think I see one missing use actually

nikomatsakis (Dec 05 2018 at 12:16, on Zulip):

oh, maybe not

lqd (Dec 05 2018 at 12:18, on Zulip):

at some point there was the question of whether or not we needed to materialize the borrows_live_at relation, it's only used in errors and we could avoid doing so with the leapjoin, so when we're not asking for these tuples (using the verbose mode flag) there was not really a need to

lqd (Dec 05 2018 at 12:22, on Zulip):

(and those might be the couple other leapjoins opportunities I remember)

nikomatsakis (Dec 05 2018 at 12:23, on Zulip):

I see

nikomatsakis (Dec 05 2018 at 12:23, on Zulip):

I think that is no longer true post bug fix

nikomatsakis (Dec 05 2018 at 12:23, on Zulip):

though you could roll that bug fix into errors I guess

nikomatsakis (Dec 05 2018 at 12:23, on Zulip):

anyway, cool

nikomatsakis (Dec 05 2018 at 12:23, on Zulip):

I might just merge the docs + publish the new datafrog

nikomatsakis (Dec 05 2018 at 12:23, on Zulip):

but first :coffee:

lqd (Dec 05 2018 at 12:24, on Zulip):

oh true, very possible that the bugfix can change things up a bit here

lqd (Dec 05 2018 at 12:37, on Zulip):

the doc comment sounds sensible to me, that the leapers propose/prevent values from their relation that should extend/filter a source tuple :thumbs_up:

lqd (Dec 05 2018 at 13:14, on Zulip):

hmm it seemed it's still true that we could fold borrows_live_at in errors. Also I might have misunderstood some leapfrog behaviour before, as I would have liked to use it to compute dying_can_reach_live: even though it works as a simple join here, the fact that it works on Relations could allow, using the leapjoin with (or not computing) borrow_live_at, to remove the need to have region_live_at duplicated in Variable/Relation forms (a long winded explanation to save one copy, albeit a potentially big one: clap has 1M+ tuples in there)

lqd (Dec 05 2018 at 13:25, on Zulip):

@nikomatsakis do you want comments on the leapjoin PR that would be like "the join allows to remove us this copy X" ? There's no real need to address such comments in this PR since it works (and also since I can make a PR later with these specific changes) so I wondered if it'd be useful or not

nikomatsakis (Dec 05 2018 at 13:27, on Zulip):

sure :)

nikomatsakis (Dec 05 2018 at 13:28, on Zulip):

I saw some copies that might be removable

nikomatsakis (Dec 05 2018 at 13:28, on Zulip):

e.g. we have subset and then two projections from it (subset_rp and some other one)

nikomatsakis (Dec 05 2018 at 13:28, on Zulip):

is that what you mean?

lqd (Dec 05 2018 at 13:28, on Zulip):

exactly

nikomatsakis (Dec 05 2018 at 13:28, on Zulip):

similarly requires

lqd (Dec 05 2018 at 13:28, on Zulip):

same as well

nikomatsakis (Dec 05 2018 at 13:28, on Zulip):

yeah, seems like only one of those projections is needed

lqd (Dec 05 2018 at 13:28, on Zulip):

those were the couple I was thinking about

nikomatsakis (Dec 05 2018 at 13:29, on Zulip):

I was debating — as an aside — whether to adjust the comments in this case to something like subset((r, p), b) instead of subset(r, p, b) or whatever

nikomatsakis (Dec 05 2018 at 13:29, on Zulip):

I think maybe keeping the datalog comments "clean"

nikomatsakis (Dec 05 2018 at 13:29, on Zulip):

but using names like subset_r2p is a decent compromise

lqd (Dec 05 2018 at 13:30, on Zulip):

I've had the same debate between being able to reuse the rules in say soufflé, and describing the precise layout/details of the datafrog computation

lqd (Dec 05 2018 at 13:31, on Zulip):

(maybe something that can be fixed with a proc-macro datafrog compiler cough cough :3)

nikomatsakis (Dec 05 2018 at 13:33, on Zulip):

:)

lqd (Dec 05 2018 at 13:59, on Zulip):

It'd be cool to have filter_maps capabilities in datafrog so that we could prevent symmetries a priori instead of hackily as I've done before. There are still some in dying_can_reach I'd like to remove, for instance.

lqd (Dec 05 2018 at 18:00, on Zulip):

(I think I mentioned this before, but I've rechecked this datapoint with datafrog 1.0: switching loc_ins to leapjoin goes from 360ms to 130ms, but doing so prevents materializing the borrow_live_at tuples the verbose mode requires)

Frank McSherry (Dec 05 2018 at 18:36, on Zulip):

It'd be cool to have filter_maps capabilities in datafrog

What sort of capabilities do you mean? In principle, it should be pretty easy to write a filter operator in datafrog (from variable -> variable) which just passes along the filtered recent set of tuples. A filter_map operator would be a bit more expensive, as you would need to re-sort, and de-duplicate w.r.t. prior tuples.

Or are you thinking of something totally different from this?

lqd (Dec 05 2018 at 18:46, on Zulip):

@Frank McSherry mostly it was a way to make this ugly hack cleaner, whether it’d be a separate filter operator, or allowing the "logic" closure to return an Option of the tuple that the join helper wouldn’t push to the results, is that clearer ?

Frank McSherry (Dec 05 2018 at 18:48, on Zulip):

I see, I think I understand. In principle, you might even like to do that at the end of the iteration, for the to_add members. The recent member is post-sorting and post-deduplication, so you may have done a bunch of work cleaning up those tuples you are about to discard.

lqd (Dec 05 2018 at 18:49, on Zulip):

(just to prevent symmetries here and there, as you rightfully pointed out before that there were many in "subsets" for example, and removing them does make a difference)

Frank McSherry (Dec 05 2018 at 18:50, on Zulip):

But, for example, the differential dataflow join allows you to specify a function FnMut(&Key, &Val1, &Val2) -> impl Iterator<Item = Result> which could possibly be helpful?

lqd (Dec 05 2018 at 18:50, on Zulip):

oh interesting

Frank McSherry (Dec 05 2018 at 18:51, on Zulip):

It might also be helpful to just have a filter method on a Variable which does the in-place filtering (so that you don't have to amend all of the join rules). You would still materialize many things in that case, but you wouldn't need as much surgery in the join rules themselves (especially good if you might have several filter predicates).

Frank McSherry (Dec 05 2018 at 18:51, on Zulip):

Adding that generality to join should be super easy. It worked great in differential, and the main change is that your join closures probably need a Some((old_result)) rather than just old_result.

lqd (Dec 05 2018 at 18:52, on Zulip):

but for sure this was the only case I seem to have wanted such a filter, it might be more interesting in fully general DD than the specific polonius use of datafrog

Frank McSherry (Dec 05 2018 at 18:53, on Zulip):

Probably the "optimal" thing to do is determine where e.g. subsets with the same scope come into existence, in terms of which rule, and augment that rule to prevent tuples containing repetition.

Frank McSherry (Dec 05 2018 at 18:54, on Zulip):

It really is a super-easy change, though. Unless I'm missing something. And in DD computations it can help a lot to avoid materializing a bunch of things that will then just be discarded. What sort of tuple reduction do you see with that filter?

lqd (Dec 05 2018 at 18:54, on Zulip):

right. (and it’s not very often)

lqd (Dec 05 2018 at 18:55, on Zulip):

I’ll need to check numbers on the computer when I’m back at it, esp if I’ve done it at the wrong time :) subsets was like 10-15% of the final count I think

Frank McSherry (Dec 05 2018 at 18:56, on Zulip):

Other easy changes: it isn't too hard to think about a Leaper implementation that doesn't contain data, just predicates. They work like the FilterAnti struct, in that they never propose anything, and only restrict proposals.

lqd (Dec 05 2018 at 18:56, on Zulip):

(and how this impacts downstream rules I hadn’t checked)

lqd (Dec 05 2018 at 18:56, on Zulip):

oh interesting as well :)

Frank McSherry (Dec 05 2018 at 18:57, on Zulip):

So when you use from_leapjoin, you could add another leaper that is just the "filter on scopes being different" leaper.

lqd (Dec 05 2018 at 18:57, on Zulip):

I stumbled upon a case I didn’t understand and which was related to filtering, I’ll investigate more details to show you if that’s ok

Frank McSherry (Dec 05 2018 at 18:58, on Zulip):

That should have the appealing property that it will filter the proposals as they flow through leapjoin, long before they get dropped into subset, long before they move from to_add into recent.

Frank McSherry (Dec 05 2018 at 18:58, on Zulip):

More details are good. Happy to help out here. :D

lqd (Dec 05 2018 at 18:59, on Zulip):

(IIRC leapjoin panicking because of a failing / max usize proposals on some specific pieces of data)

Frank McSherry (Dec 05 2018 at 18:59, on Zulip):

My main constraint is that I have no clue what the rules are doing.

Frank McSherry (Dec 05 2018 at 18:59, on Zulip):

Ooo, that sounds like a bug.

lqd (Dec 05 2018 at 19:00, on Zulip):

I’ll go home and gather more information

Frank McSherry (Dec 05 2018 at 19:00, on Zulip):

The intent is that any "well-formed" leapjoin has at least one contribution that is extend_with, so that we have positive constraints on the new values. If none have this property, it could be that all extenders say "whatever, take all values lol".

lqd (Dec 05 2018 at 19:00, on Zulip):

you, sir, are as ever quite helpful, and — literally — a scholar :D

Frank McSherry (Dec 05 2018 at 19:01, on Zulip):

np! I'll be around, and ping me elsewhere if I lose track of Zulip (which I do; every project uses a different chat site, literally no duplication yet).

lqd (Dec 05 2018 at 19:02, on Zulip):

will do, thanks again for the "filter" talk + ideas

lqd (Dec 05 2018 at 19:08, on Zulip):

(Oh that might be it, it didn’t have an extend_with IIRC, a dynamic source and 2 filter_with leapers. and that might not be well-formed at all)

Frank McSherry (Dec 05 2018 at 19:19, on Zulip):

I just pushed a branch that has an example predicate based leaper.

Frank McSherry (Dec 05 2018 at 19:21, on Zulip):

https://github.com/rust-lang-nursery/datafrog/pull/20

Frank McSherry (Dec 05 2018 at 19:23, on Zulip):

There are some other natural ones you could do, like a flat_map based leaper that proposes new values based on a function of prefix, which corresponds to integrity constraints in databases (e.g. you have a tuple with fields date, time, and datetime). Not necessarily interesting for you all, but the sort of thing that is easy-ish to do.

lqd (Dec 05 2018 at 19:27, on Zulip):

nice :)

Frank McSherry (Dec 05 2018 at 19:41, on Zulip):

Looking at the code, this rule

            subset.from_leapjoin(
                &subset_p,
                &mut [
                    &mut cfg_edge_rel.extend_with(|&(p, (_, _))| p),
                    &mut region_live_at_rel.extend_with(|&(_, (r1, _))| r1),
                    &mut region_live_at_rel.extend_with(|&(_, (_, r2))| r2),
                ],
                |&(_p, (r1, r2)), &q| (r1, r2, q),
            );

doesn't contribute any new R1 == R2 cases. Rather, the second rule

            subset.from_join(
                &live_to_dying_regions_r2pq,
                &dying_can_reach_live,
                |&(_r2, _p, q), &r1, &r3| (r1, r3, q),
            );

seems to be where they show up.

Frank McSherry (Dec 05 2018 at 19:42, on Zulip):

That means that the filter leapers probably won't help, and what you want is a join whose closure can return an impl Iterator<Item=Result> to drop r1 == r3 tuples on the floor.

lqd (Dec 05 2018 at 19:45, on Zulip):

maybe dying_can_reach_live is getting them from dying_can_reach

lqd (Dec 05 2018 at 19:46, on Zulip):

(I think the latter had some as well) the join with impl Iterator is an interesting thought indeed

Frank McSherry (Dec 05 2018 at 19:47, on Zulip):

I think that rule is

// subset(R1, R3, Q) :-
//   live_to_dying_regions(R1, R2, P, Q),
//   dying_can_reach_live(R2, R3, P, Q).

and R1 == R3 can probably happen even without dying_can_reach_live screwing things up. Maybe I misunderstand, though!

lqd (Dec 05 2018 at 19:48, on Zulip):

I have a branch somewhere to add statistics the the datafrog compute which I should refresh; might be also easy to add some predicates to check which rule and which rounds contribute to which "predicate stat"

Frank McSherry (Dec 05 2018 at 19:48, on Zulip):

But yeah it looks like dying_can_reach could get them too, from its second rule.

lqd (Dec 05 2018 at 19:54, on Zulip):

ok yeah, the case I was seeing was not well-formed, no extend leapers only filters — so I assume it's expected for it to fail.

I was modeling errors(B, P) :- requires(R, B, P), region_live_at(R, P), invalidates(P, B). as

errors.from_leapjoin(
    &requires_rp,
    &mut [
        &mut region_live_at_rel.filter_with(|&((r, p), _b)| (r, p)),
        &mut invalidates_rel.filter_with(|&((_r, p), b)| (p, b)),
    ],
    |&((_r, p), b), &()| (b, p)
);
Frank McSherry (Dec 05 2018 at 19:55, on Zulip):

Ah, ok. So this is probably painful because requires is the variable, and what you need to start from?

Frank McSherry (Dec 05 2018 at 19:56, on Zulip):

Let me ponder that. I'm sure there is a way to start from requires and "pretend" that someone has just proposed some values. At which point you can just stitch on the existing leapers, not exactly doing a join but just filtering things down.

lqd (Dec 05 2018 at 19:56, on Zulip):

yes. it's not extremely painful or anything mind you, I only stumbled upon this while trying to remove an intermediate variable, it does work perfectly otherwise :)

Frank McSherry (Dec 05 2018 at 19:57, on Zulip):

More generally, "treefrog leapjoin" is a specific instance of "delta queries", where you can implement joins and such more efficiently than the binary joins that datafrog has by default.

lqd (Dec 05 2018 at 20:00, on Zulip):

(btw my brain is now forever broken when trying to remember the join name, where I randomly mix and match pieces between it and leapfrog triejoin :)

lqd (Dec 05 2018 at 20:01, on Zulip):

inb4 a paper "a new join name, but at what COST"

lqd (Dec 05 2018 at 20:07, on Zulip):

I'm sure there is a way to start from requires and "pretend" that someone has just proposed some values

oh like an extend_with closure returning the full tuple or similar trickery ?

Frank McSherry (Dec 05 2018 at 20:10, on Zulip):

All that the rest of the leapjoin algorithm needs is a Vec<Val> for each Tuple, and so if you show up with a Relation<(Tuple, Val)> we can re-stage it temporarily as a bunch of (Tuple, Vec<Val>) for long enough for the other relations to express their opinions.

Frank McSherry (Dec 05 2018 at 20:13, on Zulip):

It needs a bit of surgery, and might look like re-writing some of leapjoin_into using the fact that you have Leaper implementations for those other relations.

Frank McSherry (Dec 05 2018 at 20:15, on Zulip):

But, if you make a note of this and collect a few of them (or just sit on this one for a while) I can try a re-think of some of the traits to accommodate more patterns that might be useful.

lqd (Dec 05 2018 at 20:16, on Zulip):

could it be something we other contribots could do (albeit with a bit of guidance I assume) so that you wouldn't have to spend time doing it ?

Frank McSherry (Dec 05 2018 at 20:19, on Zulip):

If you like, sure! Ideally, the Leaper trait is sufficient to do things like this. It is meant to capture enough info to let you dance through various candidate extensions, though it does ask for them to be in vectors, I suppose.

lqd (Dec 05 2018 at 20:20, on Zulip):

sure I'll document this case (with data, like in a test) and look for others (I think I might have had another one), to see if these requirements can be just slight surgery, which could offer new flexibility without needing to go the harder and possibly not-that-useful route of leapjoins over Variables

Frank McSherry (Dec 05 2018 at 20:21, on Zulip):

Leapjoins over variables will probably eventually show up. They really aren't that horrible, but they clash a bit with the "owned and ref unification" PR. They are the sort of thing that you would have needed back in the pre-optimized version of Polonius, where there was a self-join between subset and itself.

Frank McSherry (Dec 05 2018 at 20:22, on Zulip):

But yeah if you note down the pain points, I'm happy to help out, especially if it turns out to be pretty easy and just a bit of coding. One of the :frog: intents was that there was little enough internals that you could drop in and just screw around with vectors if you need to.

lqd (Dec 05 2018 at 20:24, on Zulip):

I was also hoping one day for fun to look at parallelizing the 3 "semi-naive evaluation joins" to see if it makes a difference on bigger relations :)

Frank McSherry (Dec 05 2018 at 20:24, on Zulip):

Actually, re-thinknig that "start from requires" issue, it could be interesting to break leapjoin into two parts: 1. a positive "propose some values" step, and then 2. "as many restrictions as you want".

Frank McSherry (Dec 05 2018 at 20:25, on Zulip):

This would allow some flexibility for how you start out, but also insist that you start from something and use types to make sure you don't lack a positive constraint on the extensions.

lqd (Dec 05 2018 at 20:29, on Zulip):

could be nice, alleviating the need for a WF check, and providing a direct place to have the "pretending someone proposed a value" before the restrictions

Jake Goulding (Dec 05 2018 at 20:41, on Zulip):

I'd like to chime in and thank y'all for this conversation. I still know nothing about all this, but this discussion was like... only 2 steps away from what I think I might know, so it's tantalizing to attempt to follow.

lqd (Dec 06 2018 at 12:07, on Zulip):

@nikomatsakis since you seem to be having fun: I think we can only have subset_pr1 and remove subset_p :)

lqd (Dec 06 2018 at 12:08, on Zulip):

(and also only requires_rp I think)

nikomatsakis (Dec 06 2018 at 12:09, on Zulip):

oh, I didn't see all these comments before =) now I see what the 'predicate leaper' was all about

nikomatsakis (Dec 06 2018 at 12:12, on Zulip):

Ah, ok. So this is probably painful because requires is the variable, and what you need to start from?

I don't follow this though

nikomatsakis (Dec 06 2018 at 12:12, on Zulip):

@lqd hmm let me take a look =) using perf stat you can definitely see some reduction (not sure if you saw my commit messages), even though removing variables doesn't seem to affect the wallclock much

nikomatsakis (Dec 06 2018 at 12:13, on Zulip):

I see, you are correct

lqd (Dec 06 2018 at 12:13, on Zulip):

yeah I did see them, at least removing the subset copies looked interesting, 3%

nikomatsakis (Dec 06 2018 at 12:17, on Zulip):

it also just seems like the code is a bit easier to understand this way

nikomatsakis (Dec 06 2018 at 12:17, on Zulip):

only one copy of the core tuples

lqd (Dec 06 2018 at 12:17, on Zulip):

I also noticed cloning the facts, which we do unequivocally in the engine, takes around 5ms on clap, not world shattering but LocationInsensitive clocks in at around 130ms here so it's not that insignificant. It could be nice to avoid it, esp. once we combine the passes, and maybe Frank's other PR about owned and ref values is a step towards this (but maybe it's just about the leapjoin so idk)

lqd (Dec 06 2018 at 12:18, on Zulip):

yes :D

nikomatsakis (Dec 06 2018 at 12:19, on Zulip):

another 0.94%

nikomatsakis (Dec 06 2018 at 12:19, on Zulip):

re: the cloning, yes, I've been thinking about it,

nikomatsakis (Dec 06 2018 at 12:19, on Zulip):

I feel like the thing to do would be to just push some of that work into the fact generation in the compiler ultimately

lqd (Dec 06 2018 at 12:19, on Zulip):

nice little win again :)

nikomatsakis (Dec 06 2018 at 12:19, on Zulip):

that said

nikomatsakis (Dec 06 2018 at 12:20, on Zulip):

well, I guess I just want to experiment with moving more of the logic into datalog

nikomatsakis (Dec 06 2018 at 12:20, on Zulip):

I'd prefer if we can get the compiler's facts to be a bit more primitive

nikomatsakis (Dec 06 2018 at 12:20, on Zulip):

and I still want to write up how the datafrog-opt rules work and investigate my proposed alternative :P which I haven't had time to do...

nikomatsakis (Dec 06 2018 at 12:21, on Zulip):

nice little win again :)

yeah

lqd (Dec 06 2018 at 12:21, on Zulip):

while things are still in flux it doesn't matter all that much rn yeah, just something on the todo list :)

nikomatsakis (Dec 06 2018 at 12:21, on Zulip):

maybe time to merge that PR

nikomatsakis (Dec 06 2018 at 12:21, on Zulip):

https://github.com/rust-lang-nursery/polonius/pull/88 I mean

lqd (Dec 06 2018 at 12:21, on Zulip):

agreed

nikomatsakis (Dec 06 2018 at 12:22, on Zulip):

(and also only requires_rp I think)

oh I can maybe do this first...

lqd (Dec 06 2018 at 12:22, on Zulip):

I do wonder about your thoughts about being able to skip generating borrows_live_at in location_insensitive and datafrogopt ?

lqd (Dec 06 2018 at 12:23, on Zulip):

it's important to have and pretty much the only thing we test at the moment, but it's not strictly speaking necessary

nikomatsakis (Dec 06 2018 at 12:25, on Zulip):

I think we should skip it

nikomatsakis (Dec 06 2018 at 12:25, on Zulip):

and test only for errors

nikomatsakis (Dec 06 2018 at 12:25, on Zulip):

we just need better tests :P

nikomatsakis (Dec 06 2018 at 12:25, on Zulip):

that's something else I've been meaning to do

nikomatsakis (Dec 06 2018 at 12:25, on Zulip):

but maybe better to open some issues

nikomatsakis (Dec 06 2018 at 12:26, on Zulip):

go through "key examples" and make more polonius unit tests from them

lqd (Dec 06 2018 at 12:26, on Zulip):

yeah :) (for datafrog_opt we might however also need the leapjoin without extend_with we mentioned yesterday as well)

nikomatsakis (Dec 06 2018 at 12:26, on Zulip):

it'd be really nice if I had any confidence that cargo test --all meant something

nikomatsakis (Dec 06 2018 at 12:26, on Zulip):

0.97%

nikomatsakis (Dec 06 2018 at 12:26, on Zulip):

(for requires)

nikomatsakis (Dec 06 2018 at 12:27, on Zulip):

leapjoin is very nice :)

lqd (Dec 06 2018 at 12:27, on Zulip):

that said, possible diagnostics work and all could impact whether we need the borrows_live_at or not

nikomatsakis (Dec 06 2018 at 12:28, on Zulip):

true, maybe

nikomatsakis (Dec 06 2018 at 12:28, on Zulip):

maybe worth waiting on that

lqd (Dec 06 2018 at 12:28, on Zulip):

once these are more clear, it could also help towards deciding whether cfg compression is good or not

nikomatsakis (Dec 06 2018 at 12:30, on Zulip):

Overall measurements from this branch on clap:

point instructions ratio
master 28,514,865,669 1.0
529b0c9 (adopt datafrog 1.0) 27,062,590,519 0.94
2df8fc3 (use only requires_rp) 21,322,189,163 0.74
nikomatsakis (Dec 06 2018 at 12:30, on Zulip):

I actually have no idea why the datafrog 1.0 switch made any difference

nikomatsakis (Dec 06 2018 at 12:30, on Zulip):

but still, 25%, not bad

nikomatsakis (Dec 06 2018 at 12:31, on Zulip):

I'll just test on rustc one last time I guess

lqd (Dec 06 2018 at 12:31, on Zulip):

there were some sorting and alloc PRs between 0.1 and 1.0 IIRC

nikomatsakis (Dec 06 2018 at 12:31, on Zulip):

ah, nice, yes

lqd (Dec 06 2018 at 12:37, on Zulip):

adding rustc's "smoke test" facts to polonius' inputs and test that it errors correctly would boost (at least my) confidence in our tests

nikomatsakis (Dec 06 2018 at 12:48, on Zulip):

seems to get the same results as before

nikomatsakis (Dec 06 2018 at 12:48, on Zulip):

merged https://github.com/rust-lang-nursery/polonius/pull/88

lqd (Dec 06 2018 at 12:49, on Zulip):

awesome job niko and frank :)

nikomatsakis (Dec 06 2018 at 13:35, on Zulip):

uh and you @lqd :P

nikomatsakis (Dec 06 2018 at 13:35, on Zulip):

ps, I didn't look at naive / location-insensitive, maybe there are leapfrog opportunities there?

lqd (Dec 06 2018 at 13:36, on Zulip):

there are indeed :) those were the reasons for the "do we generate borrows_live_at for location_insensitive" questions

lqd (Dec 06 2018 at 13:37, on Zulip):

I'll open a PR for location_insensitive later today, also probably add the smoke test just in case, and we can discuss there (I'm not imagining location_insensitive ever needing borrows like datafrogopt needs to, but you never know)

lqd (Dec 06 2018 at 20:00, on Zulip):

(the 2 remaining variants porting PRs are done, working on adding Matthew's smoke tests now)

lqd (Dec 06 2018 at 22:30, on Zulip):

(Matthew's smoke tests immediately showed a problem in the Naive variant :joy: — edit: PR fixing it is up as well)

nikomatsakis (Dec 07 2018 at 09:40, on Zulip):

(the 2 remaining variants porting PRs are done, working on adding Matthew's smoke tests now)

remind what "matthew's smoke tests" are?

lqd (Dec 07 2018 at 09:40, on Zulip):

this test

nikomatsakis (Dec 07 2018 at 09:41, on Zulip):

ah, nice

nikomatsakis (Dec 07 2018 at 09:42, on Zulip):

I just landed a PR -- hadn't noticed all of your PRs yet :P -- that adds at least one such tricky case as well (vec-push-ref)

nikomatsakis (Dec 07 2018 at 09:42, on Zulip):

link

nikomatsakis (Dec 07 2018 at 09:42, on Zulip):

though I'm only comparing against naive

nikomatsakis (Dec 07 2018 at 09:43, on Zulip):

I was thinking it'd be nice to extend the testing infrastructure to actually encode the expected results

lqd (Dec 07 2018 at 09:43, on Zulip):

I did see this cool new test case yesterday :thumbs_up: (and now I have conflicts on the cargo.lock which I had already fixed ;) slowly growing confidence in tests is nice

lqd (Dec 07 2018 at 09:44, on Zulip):

agreed, a couple tests do check the expected results but not many, if things change too much we might miss changes in expected results :/

nikomatsakis (Dec 07 2018 at 09:44, on Zulip):

yeah, it certainly makes changes to naive kind of scary

nikomatsakis (Dec 07 2018 at 09:45, on Zulip):

it's not that hard to encode expected results

nikomatsakis (Dec 07 2018 at 09:45, on Zulip):

ps @lqd I was also planning to mess a bit with applying quickcheck to datafrog, just because I've never tried using it before

lqd (Dec 07 2018 at 09:45, on Zulip):

it's surely going to be interesting :)

lqd (Dec 07 2018 at 09:46, on Zulip):

as well as datafrog unit tests, maybe benchmarks could be nice, seeing how a lot of PRs are about performance or ensuring it doesn't regress (Reed had started doing a couple last summer and we can dig them up)

lqd (Dec 07 2018 at 09:47, on Zulip):

maybe we could extend the program parser to encode expected results in the tests ergonomically

nikomatsakis (Dec 07 2018 at 10:01, on Zulip):

ps @lqd I want to merge https://github.com/rust-lang-nursery/polonius/pull/91 but it has conflicts on Cargo.lock

lqd (Dec 07 2018 at 10:01, on Zulip):

yeah I'm rebasing rn :)

nikomatsakis (Dec 07 2018 at 10:04, on Zulip):

also <https://github.com/rust-lang-nursery/polonius/pull/93> is confusing me -- the bug seems real =) but I'm confused why any of the tests are passing at all... oh test_facts is asserting that borrow_live_at is equal, ok

nikomatsakis (Dec 07 2018 at 10:05, on Zulip):

in general, I'd like to extend the tests! macro so it looks more like:

tests! {
    issue_47680("issue-47680", "main") {
        (expected error-tuples go here)
    },
    ...
}
lqd (Dec 07 2018 at 10:06, on Zulip):

the tests were mostly checking borrows_live_at indeed, checking errors we can see a difference with datafrogopt

lqd (Dec 07 2018 at 10:07, on Zulip):

all the rules were ported to generate errors, all but setting up the initial facts of a relation, thus generating no errors which the tests missed :)

nikomatsakis (Dec 07 2018 at 10:07, on Zulip):

heh

nikomatsakis (Dec 07 2018 at 10:09, on Zulip):

seems like we should just move everything over to "expected errors" and stop inspecting borrow-live-at in general

lqd (Dec 07 2018 at 10:10, on Zulip):

yeah but borrow_live_at is so valuable I wonder how to do it

lqd (Dec 07 2018 at 10:11, on Zulip):

I wish there was a way to still test them when we need to

lqd (Dec 07 2018 at 10:15, on Zulip):

(cargo.lock conflicts in PRs with multiple commits are ugh :)

nikomatsakis (Dec 07 2018 at 10:18, on Zulip):

I wish there was a way to still test them when we need to

I guess we can compute them when the dump_flags bool is true (and just duplicate a bit the rules)

lqd (Dec 07 2018 at 10:21, on Zulip):

we'd still have to have the variables and relations (albeit empty) and check whether to fill them at each compute round. that's how I've been testing its removal, but wondered about #cfgs and all

nikomatsakis (Dec 07 2018 at 10:27, on Zulip):

yes, we'd still have to do that. seems ok

nikomatsakis (Dec 07 2018 at 10:27, on Zulip):

cfg has the downside that we can't enable it dynamically

nikomatsakis (Dec 07 2018 at 10:28, on Zulip):

but I guess you might say "only do it for #[cfg(test)]" or something

nikomatsakis (Dec 07 2018 at 10:28, on Zulip):

or a cargo feature

nikomatsakis (Dec 07 2018 at 10:28, on Zulip):

I doubt the branches would be a real cost though (nor an empty variable)

lqd (Dec 07 2018 at 10:30, on Zulip):

right

lqd (Dec 07 2018 at 10:30, on Zulip):

the deps PR should be good to go now

lqd (Dec 07 2018 at 10:31, on Zulip):

(we might enjoy having bors to recheck PRs and tests :)

nikomatsakis (Dec 07 2018 at 10:38, on Zulip):

yeah could setup bors ng or something

nikomatsakis (Dec 07 2018 at 11:19, on Zulip):

ok, @lqd, https://github.com/rust-lang-nursery/polonius/pull/92 has conflicts now =)

lqd (Dec 07 2018 at 11:20, on Zulip):

:)

lqd (Dec 07 2018 at 11:20, on Zulip):

on it

lqd (Dec 07 2018 at 11:21, on Zulip):

inb4 "introducing MEGA PRs" a single PR for all one's needs

lqd (Dec 07 2018 at 11:34, on Zulip):

@nikomatsakis rebased :)

Jake Goulding (Dec 08 2018 at 17:07, on Zulip):

with applying quickcheck to datafrog

@nikomatsakis I'd recommend proptest

Jake Goulding (Dec 08 2018 at 17:08, on Zulip):

I've found it to be a bit more usable

Jake Goulding (Dec 08 2018 at 17:09, on Zulip):

Namely, the code you write to generate testcases has been more composable

nikomatsakis (Dec 11 2018 at 20:30, on Zulip):

yeah I started messing with that but got distracted

nikomatsakis (Dec 11 2018 at 20:30, on Zulip):

will try to get back to it this week maybe

Last update: Nov 21 2019 at 23:35UTC