Hacker News Reader

Comment by tinco | Hacker News Reader

So theory is not my strongest suit, maybe someone can clarify some things for me here. It seems like these equalities that we're looking for are things like the identity laws, but also extended by mathematical operations like bitshift being faster than division by 2.

Do these equalities carry all the way into general programming, to the point where we could for example say a short loop is equivalent to an unrolled loop, and thus suggest that optimization? Would we have to come up with an exhaustive list of equivalences, or is the list actually short and well known like they are in logic (Identity Laws)?

Will we at some point basically plug Egg into LLVM and have it find new optimization passes?

View on HN

Not necessarily new optimization passes, but currently the order of optimizations is more or less fixed (you can technically rearrange them between builds but almost nobody does this AFAIK except that one Uber dev optimizing iOS app size). Even worse, there is no globally optimal order as what is good for one codebase might not be optimal for another. E-graphs can find the optimum arrangement for all codebases without requiring excessive amounts of memory and so could produce better output from compilers.

They won't find new equivalences on their own though. I doubt that is even possible, you can't in general prove equivalence of functions without also solving the halting problem. Also, even just defining the equivalences we know about are often only valid in certain circumstances that I doubt a computer could figure out in the general case.

Ah that makes sense. So in LLVM's case, an optimization pass would be an equivalence.

Yes; see also the vellvm project, which develops proofs of a number of the equivalences LLVM uses: https://www.cis.upenn.edu/~stevez/vellvm/

The equivalences (between equivalent programs) correspond to specific rewrite rules. Equality saturation allows the consolidation of many such rules into a single optimization pass, without complicated ordering and assumptions, instead of arbitrary grouping that is likely to neglect opportunities.

> They won't find new equivalences on their own though.

From Tate et al 2009:

Better yet, because optimizations are allowed to freely interact during equality saturation, without any consideration for ordering, our approach can discover intricate optimization opportunities that compiler writers may not have anticipated, and hence would not have implemented in a general purpose compiler.

> > They won't find new equivalences on their own though.

> From Tate et al 2009:

> Better yet, because optimizations are allowed to freely interact during equality saturation, without any consideration for ordering, our approach can discover intricate optimization opportunities that compiler writers may not have anticipated, and hence would not have implemented in a general purpose compiler.

That's not finding new equivalences, it is finding known equivalences that are nested or composed. I suppose you could look at it as a form of unobfuscating the equivalences.

Reply on news.ycombinator.com