Stream: t-compiler/wg-polonius

Topic: subset relations and polonius


nikomatsakis (Jun 03 2019 at 17:34, on Zulip):

So I had a long chat with @Aaron Weiss today and I think we convinced ourselves that the polonius model needs a modest but non-trivial revision. The good news is that it becomes at once simpler and more precise.

nikomatsakis (Jun 03 2019 at 17:35, on Zulip):

The good news is that, in the end, we will no longer need to propagate the subset relation between points -- only the (transitive) contains relation. However, we will have to do a "pre-pass" that looks for cycles amongst the subset relations established at any point and performs unification. (Or this could potentially happen during type-check.)

nikomatsakis (Jun 03 2019 at 17:35, on Zulip):

(This will also mean @lqd that we wind up wanting to create "placeholder loans" to handle illegal subset relations.)

lqd (Jun 03 2019 at 17:37, on Zulip):

oh interesting

lqd (Jun 03 2019 at 17:38, on Zulip):

is there any bad news ? :)

lqd (Jun 03 2019 at 17:38, on Zulip):

(apart from being a non-trivial piece of work, that is)

lqd (Jun 03 2019 at 17:39, on Zulip):

do we already have an intuition about what the increased precision buys us ?

nikomatsakis (Jun 03 2019 at 17:40, on Zulip):

I think it will be better overall

nikomatsakis (Jun 03 2019 at 17:40, on Zulip):

Here is an example where existing polonius is imprecise:

nikomatsakis (Jun 03 2019 at 17:41, on Zulip):

we should check that ;)

lqd (Jun 03 2019 at 17:41, on Zulip):

(the problems prompting this change would also be interesting to learn :)

nikomatsakis (Jun 03 2019 at 17:42, on Zulip):
let mut x: &'x u32;
let mut y: &'y u32;

if something {
  y = x; // creates `'x: 'y` subset relation
}

if something {
  x = &z; // creates {L0} in 'x constraint
  // this point, we have `'x: 'y` and `{L0} in `'x`, so we also have `{L0} in 'y`
  drop(x);
}

z += 1; // polonius flags an (unnecessary) error

drop(y);
nikomatsakis (Jun 03 2019 at 17:42, on Zulip):

the problem here is that the loan L0 makes its way into 'y but it shouldn't

nikomatsakis (Jun 03 2019 at 17:43, on Zulip):

I'd be happy to schedule a call and try to talk out the intuitions here -- it was helpful to discuss with @Aaron Weiss and I imagine trying to explain it a few more times would be helpful too :)

nikomatsakis (Jun 03 2019 at 17:43, on Zulip):

which reminds me that I'm not sure if I ever posted that polonius lecture from a few days back

nikomatsakis (Jun 03 2019 at 17:43, on Zulip):

and by days I mean months or whatever :P

lqd (Jun 03 2019 at 17:44, on Zulip):

:)

nikomatsakis (Jun 03 2019 at 17:44, on Zulip):

I thinkI ran into problems because it had some errant notifications I had to edit out

lqd (Jun 03 2019 at 17:44, on Zulip):

yeah

nikomatsakis (Jun 03 2019 at 17:44, on Zulip):

and I never found a satisafactory way of doing that :)

nikomatsakis (Jun 03 2019 at 17:44, on Zulip):

despite purchasing Adobe Premiere

lqd (Jun 03 2019 at 17:44, on Zulip):

I don't think we posted this one yet

nikomatsakis (Jun 03 2019 at 17:44, on Zulip):

should just open up my mac where such stuff is easy

lqd (Jun 03 2019 at 17:44, on Zulip):

that's very understandable

lqd (Jun 03 2019 at 17:45, on Zulip):

video editing takes time, which is rare and precious :)

nikomatsakis (Jun 03 2019 at 17:45, on Zulip):

it's really rather painful on my surface

nikomatsakis (Jun 03 2019 at 17:46, on Zulip):

I'm not sure if that's windows fault, or the hardware isn't up to it, or what

lqd (Jun 03 2019 at 17:46, on Zulip):

a call with Albin also, discussing this could be nice indeed

lqd (Jun 03 2019 at 17:47, on Zulip):

(I'd need to prepare a bit, and it could be tight wrt scheduling, but definitely worthwhile)

lqd (Jun 03 2019 at 17:48, on Zulip):

that example is interesting

lqd (Jun 03 2019 at 17:52, on Zulip):

and the idea of limiting the subset TC = <3

nikomatsakis (Jun 03 2019 at 17:52, on Zulip):

the other relevant example (the one that motivated propagating subset relations in the first place) is

let v: Vec<&'v u32> = vec![];

let p: &mut Vec<&'p u32> = &mut v;
let q = &x; // creates L0
v.push(q); // adds L0 to 'p, needs to *indirectly* add to `'v`

x += 1; // should be an error
drop(v);
nikomatsakis (Jun 03 2019 at 17:53, on Zulip):

today this works because we create 'v: 'p and 'p: 'v at the &mut v point

nikomatsakis (Jun 03 2019 at 17:53, on Zulip):

and we propagate those forward

nikomatsakis (Jun 03 2019 at 17:53, on Zulip):

but the alternate we propose is to detect that cycle and basically unify 'v and 'p before polonius runs (or as a pre-pass in polonius, unclear)

nikomatsakis (Jun 03 2019 at 17:54, on Zulip):

so that the program is effectively

let v: Vec<&'v u32> = vec![];

let p: &mut Vec<&'v u32> = &mut v;
let q = &x; // creates L0
v.push(q); // adds L0 to 'v

x += 1; // is an error because `L0 in 'v` and `v` is live
drop(v);
nikomatsakis (Jun 03 2019 at 17:54, on Zulip):

(arguably a more straight-forward approach)

lqd (Jun 03 2019 at 17:55, on Zulip):

seems simpler indeed

nikomatsakis (Jun 03 2019 at 17:56, on Zulip):

it seems like it'd be potentially nice to do this in polonius, but I'm not really sure how to encode cycle detection in datafrog. I recall @Frank McSherry has some examples for differential dataflow at least though.

lqd (Jun 03 2019 at 17:56, on Zulip):

very interesting, I'll need to look into this more for sure

nikomatsakis (Jun 03 2019 at 17:57, on Zulip):

(it'd be "not terribly hard" to do on the rust side too)

lqd (Jun 03 2019 at 17:58, on Zulip):

(I wonder if Frank's recent talk was recorded/publicly available)

nikomatsakis (Jun 03 2019 at 17:58, on Zulip):

There's still something mildly bugging me about using cycles in the subset relations to decide what has to be equal but I can't quite put my finger on it. It's just strange to me that the combination of a <= b and b <= a is distinct from the effect of each statement independently (in that it kind of propagates throughout the whole graph)

nikomatsakis (Jun 03 2019 at 17:58, on Zulip):

But I think what it boils down is that there is some more precise situation when you would need equality but we don't quite have the tool to capture that

nikomatsakis (Jun 03 2019 at 17:58, on Zulip):

and maybe it doesn't matter in practice

nikomatsakis (Jun 03 2019 at 17:58, on Zulip):

I haven't come up with a good example where it would

nikomatsakis (Jun 03 2019 at 17:59, on Zulip):

(I wonder if Frank's recent talk was recorded/publicly available)

I was talking to Frank about giving a talk over Zoom at some point (a "rustc lecture series" sort of talk)

nikomatsakis (Jun 03 2019 at 17:59, on Zulip):

but we never decided on a date or topic I think :)

Frank McSherry (Jun 03 2019 at 17:59, on Zulip):

I HAVE BEEN SUMMONED!

lqd (Jun 03 2019 at 18:00, on Zulip):

I haven't come up with a good example where it would

it's also a bit harder for me to think about these in the abstract, coming up with examples in these subtle edge cases

Frank McSherry (Jun 03 2019 at 18:00, on Zulip):

What do you need to do with cycle detection, now? Like, strongly connected components, or something simpler?

Frank McSherry (Jun 03 2019 at 18:02, on Zulip):

nikomatsakis: but we never decided on a date or topic I think :)

I did a meet-up on Rust and Datalog just recently, kind of as a warm up to this. I've been thinking about it, but also not 100% sure I grok what would be most interesting and useful.

nikomatsakis (Jun 03 2019 at 18:05, on Zulip):

What do you need to do with cycle detection, now? Like, strongly connected components, or something simpler?

SCC -- we have these "subset" relations like a <= b and we would need to detect cases where, at some point P, there is a a <= b and b <= a and then "unify" a and b at all other points

nikomatsakis (Jun 03 2019 at 18:06, on Zulip):

(as I wrote above, though, it's not clear this should be done in polonius)

nikomatsakis (Jun 03 2019 at 18:08, on Zulip):

@Frank McSherry I can try to write up some pseduo-rules to better communicate what I mean, but in short I want to do a series of SCC computations and compute equality classes ("unification"-like)

nikomatsakis (Jun 03 2019 at 18:08, on Zulip):

maybe too short

Frank McSherry (Jun 03 2019 at 18:10, on Zulip):

To just throw out some information: cycle detection is pretty easy in differential dataflow, and probably also in datalog (maybe?). However, this is just the problem of detecting if there is a cycle, which can be less than what you might want.

What you might want is the strongly connected component decomposition, which assigns to each node an identifier such that nodes with the same identifier have the same transitive reachability information. Everyone in a cycle would get the same identifier, but you could have a graph with multiple cycles each of which shouldn't get the same identifiers. Because graphs may not be symmetric, you might have some cycles that can reach other cycles, but not vice-versa, and that needs to be accurately reflected.

nikomatsakis (Jun 03 2019 at 18:11, on Zulip):

we definitely more than just knowing if there is a cycle, we want to be able to say what the members are of each cycle

nikomatsakis (Jun 03 2019 at 18:11, on Zulip):

that said, the graphs are probably very small

nikomatsakis (Jun 03 2019 at 18:12, on Zulip):

so it occurs to me that something naive, like computing reachability, might suffice

nikomatsakis (Jun 03 2019 at 18:12, on Zulip):

though I would need some way to get a "representative"

nikomatsakis (Jun 03 2019 at 18:12, on Zulip):

I can sort of imagine how to do this, I guess...

nikomatsakis (Jun 03 2019 at 18:12, on Zulip):

I'll try to toy with something later on maybe

Frank McSherry (Jun 03 2019 at 18:13, on Zulip):

So, SCC computation is a packaged program in differential dataflow (https://github.com/TimelyDataflow/differential-dataflow/blob/master/src/algorithms/graphs/scc.rs) which .. it could use some love to make it a bit easier to grok the input and output ... but.

Frank McSherry (Jun 03 2019 at 18:15, on Zulip):

nikomatsakis: though I would need some way to get a "representative"

What the SCC code in DD looks like is: you show up with a graph with node identifiers, and edges between identifiers. It then does a bunch of computational magic and comes back with a collection of pairs (Node, Node) where each node exists in the first position, and has the smallest node identifier in its SCC in the second position.

Frank McSherry (Jun 03 2019 at 18:16, on Zulip):

So you get a representative for free, but it happens to be one that we choose (if there were another rule about which node identifier you want to propagate, that could work too, but "smallest" is really easy).

Frank McSherry (Jun 03 2019 at 18:16, on Zulip):

Strictly speaking, the code at the moment actually returns the edges within SCCs rather than the SCCs themselves, but .. I could fix that pretty quick if and when you want to try things out.

Frank McSherry (Jun 03 2019 at 18:17, on Zulip):

You could also just use a vanilla SCC algorithm, which will go much faster if you aren't yet at "inputs change and we want to react quickly" yet.

nikomatsakis (Jun 03 2019 at 19:23, on Zulip):

So you get a representative for free, but it happens to be one that we choose (if there were another rule about which node identifier you want to propagate, that could work too, but "smallest" is really easy).

this is roughly what I had in mind, yes.

lqd (Jun 03 2019 at 20:37, on Zulip):

would we expect the motivating example to fail in Polonius today, or would it require supporting illegal subset relations errors ?

Albin Stjerna (Jun 03 2019 at 20:55, on Zulip):

(I saw this conversation, but I'm going to bed so I'll read it properly tomorrow!)

lqd (Jun 03 2019 at 21:13, on Zulip):

(I'm not seeing it yet, and expected L0 to be killed after the 2nd if, so no unnecessary Polonius error here :thinking: ?)

nikomatsakis (Jun 03 2019 at 21:14, on Zulip):

@lqd did you actually try it?

lqd (Jun 03 2019 at 21:15, on Zulip):

yes :/

nikomatsakis (Jun 03 2019 at 21:15, on Zulip):

I would expect an error today, but it may take a bit of tweaking to set it up correctly :)

lqd (Jun 03 2019 at 21:15, on Zulip):

right

lqd (Jun 03 2019 at 21:15, on Zulip):

the tweaking must be what I'm missing indeed

nikomatsakis (Jun 03 2019 at 21:16, on Zulip):

what is the example as you have it setup?

lqd (Jun 03 2019 at 21:16, on Zulip):

say, this will faill with just nlls but work in Polonius

lqd (Jun 03 2019 at 21:18, on Zulip):

(eternal personal reminder to add -Z support to the playground)

nikomatsakis (Jun 03 2019 at 21:18, on Zulip):

(it's also worth noting that I could be missing something)

nikomatsakis (Jun 03 2019 at 21:19, on Zulip):

but ok I think I see why it's not reproducing, let me think about the most elegant variant :)

nikomatsakis (Jun 03 2019 at 21:19, on Zulip):

I guess I can test this wth -Zpolonius myself

lqd (Jun 03 2019 at 21:21, on Zulip):

(I did have a mockup with -Z support to the playground, and eddy often asks ;)

nikomatsakis (Jun 03 2019 at 21:22, on Zulip):

I think something like this is probably good: playground

nikomatsakis (Jun 03 2019 at 21:23, on Zulip):

I basically just changed from let mut x: &u32 to let mut x: (&u32,) = ...

nikomatsakis (Jun 03 2019 at 21:23, on Zulip):

so that the x.0 = ... doesn't completely kill

nikomatsakis (Jun 03 2019 at 21:23, on Zulip):

you could probably make a more realistic example with vec![] and push or something

nikomatsakis (Jun 03 2019 at 21:23, on Zulip):

I think the new formulation I am proposing would handle the example above

lqd (Jun 03 2019 at 21:24, on Zulip):

ah yes, it does trigger thanks a lot

lqd (Jun 03 2019 at 21:26, on Zulip):

I think the new formulation I am proposing would handle the example above

maybe we can prototype it "quickly"

nikomatsakis (Jun 03 2019 at 21:32, on Zulip):

Hmm, yes.

nikomatsakis (Jun 03 2019 at 21:34, on Zulip):

it'd be useful if we added some min-like operators to datafrog somewhere

nikomatsakis (Jun 03 2019 at 21:34, on Zulip):

question is precisely where :)

nikomatsakis (Jun 03 2019 at 21:41, on Zulip):

well you know

nikomatsakis (Jun 03 2019 at 21:41, on Zulip):

we could pretty easily write the code we need in polonius in rust I guess

lqd (Jun 03 2019 at 21:47, on Zulip):

(yeah that's what I was thinking as well, I was wondering about the updated rules, if we just needed to simply not do the subset TC — probably not)

lqd (Jun 04 2019 at 00:14, on Zulip):

( :up: was misspoken, as IIRC the TC at a single point would not change, but propagating subsets along the CFG would not be necessary anymore)

Albin Stjerna (Jun 04 2019 at 09:55, on Zulip):

we could pretty easily write the code we need in polonius in rust I guess

There is a great joke here about everyone rewriting their C(++) stuff in Rust, and the Rust people now basically inventing something else to rewrite parts of Rust in because Rust is already in Rust

Albin Stjerna (Jun 04 2019 at 15:58, on Zulip):

Ok, I have read through this but not fully digested it. I think I'll need some more examples and/or careful deductions on paper (for/by myself) to figure this out. Which is good, because it reminds me that I should go through the actual borrow check logic and make sure I understand it too, and not just the parts I'm working on.

lqd (Jun 04 2019 at 16:13, on Zulip):

(same for me ;)

lqd (Jun 05 2019 at 16:50, on Zulip):

in case it's useful, this should be a small program which would need subsets to be propagated along the CFG to emit an error:

universal_regions { }
block B0 {
    outlives('r1: 'r0);
    borrow_region_at('r2, L0), outlives('r2: 'r1), region_live_at('r0), region_live_at('r1);
    invalidates(L0), region_live_at('r0);
}
lqd (Jun 05 2019 at 16:52, on Zulip):

(I think :p)

lqd (Jun 05 2019 at 20:47, on Zulip):

and if we need more examples, the vec-push-ref cases in our input facts dataset also need this CFG propagation (and they're similar to the examples at the start of this thread)

lqd (Jun 05 2019 at 20:49, on Zulip):

(I seem to have lost my bugpoint-like tool for helping reduce NLL facts automatically; I might have to reduce datalog facts manually like they used to do in the 18th century)

nikomatsakis (Jun 06 2019 at 00:33, on Zulip):

and if we need more examples, the vec-push-ref cases in our input facts dataset also need this CFG propagation (and they're similar to the examples at the start of this thread)

I was just thinking about this example

nikomatsakis (Jun 06 2019 at 00:33, on Zulip):

and wondering how it related

nikomatsakis (Jun 06 2019 at 00:37, on Zulip):

btw @lqd I think polonius#107 describes a way to prototype this idea

lqd (Jun 06 2019 at 06:36, on Zulip):

thanks for writing that up :) I'll look at it in more detail later today. I don't have the intuition yet that we only needed the propagation for equal regions

nikomatsakis (Jun 06 2019 at 09:48, on Zulip):

Noticed an interesting example, described here. I'm curious @Aaron Weiss what the Oxide type system would do here.

lqd (Jun 06 2019 at 10:49, on Zulip):

(in a rare display of bad luck, reducing the "propagating subsets along the CFG is sometimes necessary"-case -- ensuring the error is emitted -- effectively turned it into the "propagating subsets along the CFG is sometimes imprecise"-case, so my previous example shows the error which shouldn't appear)

nikomatsakis (Jun 06 2019 at 12:15, on Zulip):

Noticed an interesting example, described here. I'm curious Aaron Weiss what the Oxide type system would do here.

to continue on this point though, even if equal must be propagated along the CFG, that is still potentially more efficient that subset. This is because the equal relation is reflexive, so in principle we ought to be implement it nicely.

One related thing I've been wondering about is the connection to liveness. A key part of the polonius analysis is removing tuples that touch on dead regions, but that feels like it is serving a similar purpose to this new twist -- i.e., helping to separate "instantaneous behavior" from a "continuous connection". (Witness that to reproduce the imprecision in my origin example, I had to introduce tuples to sidestep the liveness analysis.)

Aaron Weiss (Jun 06 2019 at 15:46, on Zulip):

Noticed an interesting example, described here. I'm curious Aaron Weiss what the Oxide type system would do here.

Since Oxide only requires type information to be on the same page at the end of the branches, I think this example should work in a fairly straightforward manner. Locally, within each branch, the provenance stuff works out, and at the end of the branch, they both agree on the state of the world (so there's not even a question of "whether or not unifying the two states will succeed").

lqd (Jun 06 2019 at 18:42, on Zulip):

(I quickly prototyped this and it seems to pass the repo's tests — I wasn't able to try on rustc's yet. In particular the vec-push-ref ones pass, and they seem to depend on cfg propagation for some reason — still unsure why as of now. Still, I must have made some mistake in that it may not be working/OOMs on clap)

nikomatsakis (Jun 06 2019 at 22:20, on Zulip):

the question @Aaron Weiss is whether the type of p, a and b will have to use the same provenance for the &u32

Aaron Weiss (Jun 06 2019 at 22:22, on Zulip):

Ah, I think with how T-Assign is setup right now, the answer is yes.

Aaron Weiss (Jun 06 2019 at 22:25, on Zulip):

Actually, I'm not so sure. It might work in Oxide if they're different as long as they're provenances that _can_ unify (i.e. they're not unrelated parameterized provenance variables).

Aaron Weiss (Jun 06 2019 at 22:25, on Zulip):

This is definitely something I should try when I actually manage to get the implementation working.

lqd (Jul 09 2019 at 09:41, on Zulip):

I worked on this last night, and even if I’m not 100% sure of the new behavior (I feel it’s computing a lot more "requires" than before, therefore slower) I also had a tiny thought that had some interesting results: historically we used to compute every "borrow_live_at", and I didn’t expect limiting those to only track invalidated loans would be that impactful. With this, the prototype passes clap fast (most of the new computation seems about previously untracked regions, and is mostly ignored with this filter), and so I also tried tracking equality across the CFG, and that seems to work as well, no "polonius-imprecision unnecessary-error" or with your example in the issue "polonius-imprecision flow-sensitive-equality-required" @nikomatsakis :) I’ll test in rustc later today, these tests were only in the polonius inputs.

lqd (Jul 09 2019 at 09:50, on Zulip):

(I'm not sure on how exactly to control the equality propagation yet, and it might be a coincidence that both tests and the new issue pass, until I've verified in rustc; but I only propagated equality in the cfg if both equal regions were live at the end point of the edge — this might indeed require changing)

nikomatsakis (Jul 09 2019 at 10:12, on Zulip):

@lqd I'm not quite sure what you mean -- you implemented the filter on the existing rules, you mean?

nikomatsakis (Jul 09 2019 at 10:12, on Zulip):

Is this code in an open PR?

lqd (Jul 09 2019 at 10:14, on Zulip):

yes, on both the existing rules and the different versions of the prototype; not yet in a PR though, it's on top of this branch

lqd (Jul 09 2019 at 10:14, on Zulip):

I can update the branch if you want ?

nikomatsakis (Jul 09 2019 at 10:26, on Zulip):

I'm a bit wary of said filter changing behavior

nikomatsakis (Jul 09 2019 at 10:27, on Zulip):

Unless you're saying that it's just running faster but getting same results

nikomatsakis (Jul 09 2019 at 10:27, on Zulip):

I guess i'd like to take a look at the original, unfiltered version of your new analysis

lqd (Jul 09 2019 at 10:27, on Zulip):

I hope it's not changing results but will check on the test suite later today

nikomatsakis (Jul 09 2019 at 10:27, on Zulip):

is that still in the branch? it's something I've been meaning to return to

lqd (Jul 09 2019 at 10:28, on Zulip):

but basically what I mean is I'm filteting borrow regions to only look at loans which might be invalidated

lqd (Jul 09 2019 at 10:28, on Zulip):

that changes results of computing all the borrow live at tuples, but those are only useful joined with invalidations

lqd (Jul 09 2019 at 10:29, on Zulip):

that is, I feel I'm only tracking the loans which matter now, instead of all loans

nikomatsakis (Jul 09 2019 at 10:29, on Zulip):

Cool -- definitely something I wanted to try doing.

nikomatsakis (Jul 09 2019 at 10:30, on Zulip):

I'm not really sure what my expectations were, but I can imagine it being a big win

lqd (Jul 09 2019 at 10:30, on Zulip):

a bit like we talked about reusing the results of the location insensitive analysis, limiting the full analysis to only those loans; instead it's the limiting it to the invalidated loans

lqd (Jul 09 2019 at 10:30, on Zulip):

again I hope to validate rustc's behavior with the tests first but it was interesting yes :)

nikomatsakis (Jul 09 2019 at 10:30, on Zulip):

a bit like we talked about reusing the results of the location insensitive analysis, limiting the full analysis to only those loans; instead it's the limiting it to the invalidated loans

yeah good point, maybe we didn't consider this variant? I can't remember.

lqd (Jul 09 2019 at 10:31, on Zulip):

it doesn't ring a bell which is weird cause it seems "obvious"

nikomatsakis (Jul 09 2019 at 10:31, on Zulip):

Indeed

nikomatsakis (Jul 09 2019 at 10:31, on Zulip):

Ah well

lqd (Jul 09 2019 at 10:31, on Zulip):

but we've prototyped the other information sharing in the hybrid variant

nikomatsakis (Jul 09 2019 at 10:31, on Zulip):

I think maybe this arises from

nikomatsakis (Jul 09 2019 at 10:31, on Zulip):

&*x where x: &T?

nikomatsakis (Jul 09 2019 at 10:32, on Zulip):

i.e., if you borrow &x and x is immutable, it will have a StorageDead that invalidates it

nikomatsakis (Jul 09 2019 at 10:32, on Zulip):

but if you are borrowing &*x it may never

nikomatsakis (Jul 09 2019 at 10:32, on Zulip):

we optimize this case in "normal" NLL, too

lqd (Jul 09 2019 at 10:32, on Zulip):

still feels strange that this kinda fixes the prototype on clap (so I'd like to investigate more here ofc; that might mean that clap is fine but some other case where most borrow regions are invalidated will still be slow on datafrogopt or the prototype)

nikomatsakis (Jul 09 2019 at 10:33, on Zulip):

yeah this may be a good optimization but perhaps ultimately less good than the insensitive variant (and, of course, you could probably apply it there too, no?)

lqd (Jul 09 2019 at 10:39, on Zulip):

I did yeah :)

lqd (Jul 09 2019 at 10:39, on Zulip):

everywhere

lqd (Jul 09 2019 at 10:40, on Zulip):

it's a bit subtle to see since the borrow regions are straight out of rustc, so the relation's content is a bit most obvious there

lqd (Jul 09 2019 at 10:57, on Zulip):

here's the updated prototype niko: link

lqd (Jul 09 2019 at 10:59, on Zulip):

still feels like it might work thanks to luck, so I'll want to understand more of the behaviour without this filtering (and without the flow sensitive equality present in this commit)

lqd (Jul 09 2019 at 10:59, on Zulip):

but it seemed like it was tracking at least 10x more requires

nikomatsakis (Jul 09 2019 at 11:01, on Zulip):

here's the updated prototype niko: link

this is pre-optimization, right?

nikomatsakis (Jul 09 2019 at 11:01, on Zulip):

but it seemed like it was tracking at least 10x more requires

I wanted to check how you implemented it, this seems plausible, but I suspect we can cut it down in other ways too

lqd (Jul 09 2019 at 11:01, on Zulip):

actually, it's with the optimization

nikomatsakis (Jul 09 2019 at 11:01, on Zulip):

ah ok

lqd (Jul 09 2019 at 11:02, on Zulip):

the optimization is this

nikomatsakis (Jul 09 2019 at 11:03, on Zulip):

+1

lqd (Jul 09 2019 at 11:03, on Zulip):

I fear it's just optimizing clap tho :)

lqd (Jul 09 2019 at 11:03, on Zulip):

(or cases where the set of invalidated loans is lower than the set of borrow regions' loans, say)

nikomatsakis (Jul 09 2019 at 11:04, on Zulip):

well, if it's the &*x case that I was describing, then I think it's more general than that

lqd (Jul 09 2019 at 11:04, on Zulip):

I'd like to investigate if it's those indeed

nikomatsakis (Jul 09 2019 at 11:04, on Zulip):

though I suspect the best would be to (a) use this optimization for the flow insensitive variant and then (b) use results from flow insensitive variant to inform the flow sensitive version

lqd (Jul 09 2019 at 11:04, on Zulip):

yeah true

lqd (Jul 09 2019 at 11:06, on Zulip):

optimizations while the correctness story is still a bit in flux feels strange, but we've already prototyped the sharing between the 2 variants so I'm not worried we can do these easy and effective optimizations there

lqd (Jul 09 2019 at 11:10, on Zulip):

I have hopes to do a lot of this before you return from vacation :)

lqd (Jul 09 2019 at 11:11, on Zulip):

(ofc the prototype is terrible WIP, I split it into 2 computations just so I could control the equality in rust, but it's probably doable in datafrog)

lqd (Jul 09 2019 at 11:12, on Zulip):

(I gtg for a bit and then I can test this in rustc)

lqd (Jul 09 2019 at 17:14, on Zulip):

ran this variant on rustc tests, only 15 more failures, impressive

lqd (Jul 09 2019 at 17:14, on Zulip):

some of them look bad though, like compiling things which probably shouldn't compile :)

lqd (Jul 09 2019 at 17:17, on Zulip):

polonius is like "you may not like it but this is what peak borrowcking looks like" -- I'll thin those out over the summer, so we know why it's doing this, probably just bugs rather than unsoundness (otherwise we might have heard about it from aatxe)

Last update: Nov 15 2019 at 20:10UTC