Stream: t-compiler/wg-polonius

Topic: datalog interpreter impl


Gus Wynn (Dec 08 2020 at 00:25, on Zulip):

https://twitter.com/guswynn/status/1336091790223368194?s=20

why does chalk have its own solver, but polonious uses datafrog? Is it for perf and datafrog makes proof of concepts easier? Chalk and polonious both use datalog right? or does chalk need something higher than datalog?

lqd (Dec 08 2020 at 01:37, on Zulip):

chalk’s is different and more prolog like indeed, not datalog. datafrog was actually made for polonius, so it is Polonius’ solver in that way

lqd (Dec 08 2020 at 01:41, on Zulip):

(polonius did not exist as such then, only as experiments within NLLs, but the datalog engine was made to replace the timely-dataflow based implementation of these experiments, which live on as polonius)

Gus Wynn (Dec 08 2020 at 16:31, on Zulip):

if prolog is a super-set datalog, why not merge the core engine parts of chalk and polonious?

lqd (Dec 08 2020 at 16:51, on Zulip):

Chalk's solver also goes a bit beyond prolog's clauses

lqd (Dec 08 2020 at 16:51, on Zulip):

it's not only Horn clauses

lqd (Dec 08 2020 at 16:52, on Zulip):

but one generalisation: Hereditary Harrop formulas/predicates

lqd (Dec 08 2020 at 16:52, on Zulip):

we do need some of those for Rust, but that job can be shared between chalk and polonius

lqd (Dec 08 2020 at 16:53, on Zulip):

so the current line of thought is (and bear in mind this is where we have done the least design work or prototyping as of now)

lqd (Dec 08 2020 at 16:55, on Zulip):

to have them collaborate, rather than merged into one, chalk's handling higher-ranked subtyping and generating "current polonius" facts

lqd (Dec 08 2020 at 16:56, on Zulip):

in particular it's not absolutely set in stone that we're going to use a datalog engine to do the different polonius analyses

bjorn3 (Dec 08 2020 at 16:56, on Zulip):

There is a big difference between prolog and datalog. Prolog starts at the goal and works down towards facts that could satisfy them. Datalog starts with facts and repeatedly applies the rules until no further facts can be discovered. Chalk has to use prolog as the set of derivable facts is often infinite. This is not the case for polonious, so datalog can be used, which could be more efficient.

lqd (Dec 08 2020 at 16:56, on Zulip):

it's what we use now, because it's extremely easy to prototype, concise, clear and relatively performant to do so

lqd (Dec 08 2020 at 16:57, on Zulip):

but it's also currently not exactly scaling to what we need it to, so we'll see how this shakes out

lqd (Dec 08 2020 at 16:58, on Zulip):

(Niko has a post on concerns about higher-ranked subtyping if you're interested https://smallcultfollowing.com/babysteps/blog/2019/01/21/hereditary-harrop-region-constraints/)

lqd (Dec 08 2020 at 17:00, on Zulip):

(technically both directions of evaluation can work in datalog, the "top-down evaluation" is the most prolog-y, and the "bottom-up evaluation" is exactly how bjorn3 described -- and datafrog is currently the latter kind)

lqd (Dec 08 2020 at 17:08, on Zulip):

just to illustrate why, even though we love the benefits of datalog, it's not necessarily the greatest solution to everything: the location insensitive analysis can be reframed as another problem, and if anyone knows a datalog engine that will do that, detect arbitrary rules and transform them into reachability queries on the condensation graph of the CFG, with bonus points if it computes the SCCs and the reachability acceleration structure at the same time, like Nuutila's modified Tarjan's method, please let me know :)

lqd (Dec 08 2020 at 17:10, on Zulip):

(also the queries need to not allocate)

Gus Wynn (Dec 08 2020 at 17:15, on Zulip):

interesting, my concern/thinking was that while a datalog engine could be more efficient, more time may have been spent on the efficiency of the chalk solver then it may still be faster than datafrog (obviously this is not tested), and it could be less code to maintain, but i see now its much more subtle that than

as well as what @lqd said, for prototyping, simplicity is key for now

Gus Wynn (Dec 08 2020 at 17:16, on Zulip):

lqd said:

to have them collaborate, rather than merged into one, chalk's handling higher-ranked subtyping and generating "current polonius" facts

wait chalk and polonious will have to interact? or will chalk have to produce some info about sub-typing that polonious has to be given?

lqd (Dec 08 2020 at 17:17, on Zulip):

since they compute different things it's not easy to compare them on efficiency, but in truth not that much has been done on efficiency in either solvers; mostly because correctness needs to come first in these sensitive cases

Gus Wynn (Dec 08 2020 at 17:17, on Zulip):

lqd said:

just to illustrate why, even though we love the benefits of datalog, it's not necessarily the greatest solution to everything: the location insensitive analysis can be reframed as another problem, and if anyone knows a datalog engine that will do that, detect arbitrary rules and transform them into reachability queries on the condensation graph of the CFG, with bonus points if it computes the SCCs and the reachability acceleration structure at the same time, like Nuutila's modified Tarjan's method, please let me know :smile:

this is an interesting comment and I clearly have a lot to learn about

Gus Wynn (Dec 08 2020 at 17:17, on Zulip):

lqd said:

since they compute different things it's not easy to compare them on efficiency, but in truth not that much has been done on efficiency in either solvers; mostly because correctness needs to come first in these sensitive cases

ah

Gus Wynn (Dec 08 2020 at 17:19, on Zulip):

I think im going to re-read every chalk and polonious post niko has made this week

lqd (Dec 08 2020 at 17:20, on Zulip):

again, not that much has been done on these advanced topics (as we haven't finished handling the most basic topics yet), and of course Niko was the one doing that, so take this with a grain of salt :) my recollection is that chalk will produce polonius facts and interact with it while solving higher-ranked stuff

lqd (Dec 08 2020 at 17:21, on Zulip):

there has been chalk branches in that direction, and some design work, so one could say it's still in the design phase ^^ there's a plan, but until we either have the time to devote to the topic, or chalk is finished and there's nothing else to do but look at that, it's still a tentative plan

lqd (Dec 08 2020 at 17:23, on Zulip):

unfortunately life gets in the way and none of us have a lot of time available to dedicate to polonius; this is why we have this different sprint model where we periodically make the time and hack together. hopefully we can pick that up early next year once things clear up for everybody

lqd (Dec 08 2020 at 17:24, on Zulip):

I hope that answers your questions

Gus Wynn (Dec 08 2020 at 17:24, on Zulip):

yeah to be clear, i wasnt expecting anything soon, just getting my bearing to see if I can help out at some point!
glad to hear next year there might be interesting stuff happening!

Gus Wynn (Dec 08 2020 at 17:24, on Zulip):

lqd said:

I hope that answers your questions

it does, thanks!!

lqd (Dec 08 2020 at 17:24, on Zulip):

sure, no problem

Last update: Jun 20 2021 at 01:15UTC