Stream: t-compiler/wg-polonius

Topic: Endgame for Polonius?


ecstatic-morse (Jan 01 2021 at 19:30, on Zulip):

Is the general consensus that the culmination of the Polonius effort will include an embedded datalog solver in rustc? Or is datalog just meant for prototyping the "sets of loans" approach to borrow-checking? My assumption is the former, since otherwise I don't see a reason to have datalog versions of liveness/initialization: those problems are already well understood. Having a datalog solver would also make it easier to implement other analyses (pointer analysis for mir-opt comes to mind). On the other hand, it will be very difficult to make the datalog version execute as fast as a hand-optimized version, so there will be pressure to switch if/when the final semantics are decided on.

The answer to this determines how much effort I'm willing to spend trying to speed up the datafrog and/or the Polonius rules.

lqd (Jan 01 2021 at 21:51, on Zulip):

this is a question that is hard for me to answer unfortunately: I'll try to summarize, and be extra clear when things are my opinion, and when there's consensus

lqd (Jan 01 2021 at 21:54, on Zulip):

I think the endgame plan is not yet set in stone. I think the consensus would be that if we could get away with it, we would.

lqd (Jan 01 2021 at 21:56, on Zulip):

That is, we do have the prototyping use-case you mention, absolutely. And if that prototype was acceptable to use in production, I can't think of why we wouldn't use it.

lqd (Jan 01 2021 at 22:00, on Zulip):

There's also value in having "the whole of the borrow checker" in a single, easy to understand place (that's a bit handwavy as so much of that behaviour also depends on rust-to-MIR and MIR-to-facts lowering, NLL-constraints-to-facts lowering, etc), and in a library that others could use, say rust-analyzer in an ideal world

lqd (Jan 01 2021 at 22:02, on Zulip):

so those are why we currently have re-done the parts you mention, with the results you mention, it is indeed hard to match the already existing versions.

lqd (Jan 01 2021 at 22:02, on Zulip):

whether that's enough of a justification we're not sure

lqd (Jan 01 2021 at 22:03, on Zulip):

at least those are the goals

lqd (Jan 01 2021 at 22:05, on Zulip):

my own thoughts are: as things stand today, I'm not sure we can get away with it. I don't know what your dataflow expertise tells you about this question ?

lqd (Jan 01 2021 at 22:06, on Zulip):

we also lack information to have an informed opinion: we lack both data and benchmarks.

lqd (Jan 01 2021 at 22:08, on Zulip):

we also don't know our "budget": what is considered an acceptable cost for the increased precision we'd gain

lqd (Jan 01 2021 at 22:16, on Zulip):

especially thinking this cost is hard to quantify in practice: we have access to a lot of code and benchmarks that do compile. The vast majority of that will pass the location insensitive analysis: modulo some subtlety about fact generation, more dialogue between rustc and polonius to possibly avoid some work, all those will be super fast. Whenever there's a "potential error" (either of 2 kinds) we'll also be able to heavily filter the data that does not contribute to these 2 errors, making even the location-sensitive analyses "not that slow"

lqd (Jan 01 2021 at 22:17, on Zulip):

This is also why we have been focusing on correctness and completeness, before focusing on performance

lqd (Jan 01 2021 at 22:21, on Zulip):

but they are ultimately related in the "if we can't pull it off, what do we do" sense, and this is where I've been focusing most of my efforts (trying to come up with different ways of making that work and failing at that a whole lot) rather than move errors or liveness.

lqd (Jan 01 2021 at 22:22, on Zulip):

if that happens, the rules and datafrog will still be invaluable as reference implementations whose behaviour we need to match

lqd (Jan 01 2021 at 22:23, on Zulip):

sorry for the brain dump @ecstatic-morse I hope it was somewhat coherent, but that question probably needs @nikomatsakis

Last update: Jun 20 2021 at 00:15UTC