kmeakin (Apr 18 2023 at 00:22): kmeakin (Apr 18 2023 at 00:22):Do we have any policy on circular egraph rewrite rules (ie rule 1 matches on the RHS of rule 2, and rule 2 matches on the RHS of rule 1)?
kmeakin (Apr 18 2023 at 00:25):In particular, I want a rule like
ineg(select(cond, x, y)) => select(cond, ineg(x), ineg(y))
and also select(cond, ineg(x), ineg(y)) => ineg(select(cond, x, y))
Jamey Sharp (Apr 18 2023 at 00:46):The good news is that shouldn't lead to much extra computation. If one rule fires then the other one will too, but the second one will only build instructions which are already in the GVN map, so they won't be passed through the ISLE rules a third time.
Jamey Sharp (Apr 18 2023 at 00:49):We're still figuring out what makes "good" rules in our particular version of the egraph framework, and I don't think we've tried any pairs of rules of that form yet. So maybe the answer is we should try it and find out whether it has a significant effect. But I'm curious whether @Chris Fallin already has informed guesses about how that experiment will go.
Chris Fallin (Apr 18 2023 at 00:53):The only thing that we need to avoid is a "generative" situation where, e.g., we rewrite x => x + 0. Without limits, that would recurse infinitely. We have a backstop to that sort of issue with our rewrite-depth limit (currently 5), just in case
Chris Fallin (Apr 18 2023 at 00:56):One other issue that arises in cases like this is cost vs. payoff. As a very handwavy and not-formal-at-all sort of guideline, I think we probably want to write rules that have clear directionality (in an, err, thermodynamic sense of sorts -- toward simpler programs). Or said another way, a rule might be good if the thing it rewrites to (or another rewrite that it unlocks) is more likely to be chosen during extraction than the original. On the other hand, a rule like a generic commutativity rule (e.g., for every iadd(a, b), rewrite to iadd(b, a) too) will (again, handwavily) lead to better cases 50% of the time at most, and just adds an extra node (and the matching cost on it) otherwise
Chris Fallin (Apr 18 2023 at 00:57):That does preclude some of the emergent magic that can happen in full equality saturation of course, so maybe there's another mode or set of rules that we do enable when we want "perfect optimization"
kmeakin (Apr 18 2023 at 00:59):Chris Fallin said:
One other issue that arises in cases like this is cost vs. payoff. As a very handwavy and not-formal-at-all sort of guideline, I think we probably want to write rules that have clear directionality (in an, err, thermodynamic sense of sorts -- toward simpler programs). Or said another way, a rule might be good if the thing it rewrites to (or another rewrite that it unlocks) is more likely to be chosen during extraction than the original. On the other hand, a rule like a generic commutativity rule (e.g., for every
iadd(a, b), rewrite toiadd(b, a)too) will (again, handwavily) lead to better cases 50% of the time at most, and just adds an extra node (and the matching cost on it) otherwise
What about guarding such rewrite rules to only apply if the rewrite triggers further rewrites?
eg
(rule (simplify (unop ty op (select _ cond x y)))
(if-let _ (simplify (select ty cond (unop ty op x) (unop ty op y)))
(select ty cond (unop ty op x) (unop ty op y)))
ah, definitely not, we don't want to invoke simplify recursively inside of simplify -- that is a recipe for unexpected runaway rewrites
Chris Fallin (Apr 18 2023 at 01:07):and such a question would require backtracking (if a new node doesn't simplify to anything interesting then... delete it?); and we've already spent the time invoking rewrite rules on it anyway
Chris Fallin (Apr 18 2023 at 01:08):fwiw, I haven't studied the latest PRs in detail, but we do have precedent for rules that aren't obviously better by themselves if they "herd terms in the right direction" -- e.g., we have DeMorgan that pushes bnot downward, past or/and, to try to combine with other things
Chris Fallin (Apr 18 2023 at 01:08):as long as we're consistent in that direction, it seems reasonable
kmeakin (Apr 18 2023 at 01:17):I don't think either direction is obviously better:
ineg(select(cond, x, y)) is probably faster in the general case,
but select(cond, ineg(x), ineg(y)) could reveal further rewrites (eg if x or y are constants)
Chris Fallin (Apr 18 2023 at 01:20):one way to resolve the question objectively is just to test! trying to see if the rule improves anything in the Sightglass suite would be interesting
kmeakin (Apr 18 2023 at 02:09):I'll try that in the morning
kmeakin (Apr 18 2023 at 02:10):Btw why don't we support generative rewrites? IIRC EGG supports generative rewrites
Chris Fallin (Apr 18 2023 at 08:08):Well, it's not that we don't support it; nothing in the infrastructure will prevent you from writing such a rule, and it will even execute and produce more nodes. But the reasoning is exactly what I wrote above: it leads to blowup.
Chris Fallin (Apr 18 2023 at 08:08):Imagine the simple rule x => x + 0. It can be iterated infinitely many times; the only reason the optimization would terminate with such a rule is our backstop limit on rewrite depth
Chris Fallin (Apr 18 2023 at 08:09):That's why we (by convention) don't write such rules
kmeakin (Apr 19 2023 at 23:31):Chris Fallin said:
Imagine the simple rule
x => x + 0. It can be iterated infinitely many times; the only reason the optimization would terminate with such a rule is our backstop limit on rewrite depth
I think EGG handles that by allowing e-classes to have loops
Jamey Sharp (Apr 19 2023 at 23:54):You're right: in egg, x => x + 0 will match every e-node, but for a given x it will only create one x + 0 e-node. Once that's unioned into the same e-class as x, when the rule fires again to create (x + 0) + 0, it'll notice that the left-hand side is equivalent to x and then that x + 0 is already in the GVN map, and it won't create another e-node. That still allows a rule like (x + y) + z to match x because the matcher can follow cycles in the e-graph. It also makes extraction difficult, which is a big part of why we disallow cycles in Cranelift's e-graph implementation.
kmeakin (Apr 20 2023 at 00:25):I see
Last updated: Nov 22 2024 at 16:03 UTC