llvm dev - Sep 2017 - InstCombine, graph rewriting, Equality saturation

Hello all,

I've seen some discussion that InstCombine is "too general" and
that llvm
should implement a proper graph rewrite mechanism:

Link to llvm-dev discussion about this:
http://lists.llvm.org/pipermail/llvm-dev/2017-May/113219.html,
Link to review where this came up (and I first heard about it):
https://reviews.llvm.org/D37195.

I wanted to understand what the current issues with InstCombine are, and if
a graph rewriter prototype is something people are interested in. I find
the idea appealing, from what little I know it, so I'd be interested in
hacking something up.

What would such a framework look like? Is there past literature on the
subject? From what I know, many functional compilers using combinator based
compilation were graph rewriting. Is there other prior art?

Also, there is the idea of Equality Saturation (
http://www.cs.cornell.edu/~ross/publications/eqsat/) that I found out about
recently. Could this be used to augment the InstCombine infrastructure?

Thanks,
~Siddharth

-- 
Sending this from my phone, please excuse any typos!
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
<http://lists.llvm.org/pipermail/llvm-dev/attachments/20170905/80d0f820/attachment.html>

Equality saturation is very cool work and Ross Tate mentioned to me that 
he'd be happy to chat with you about this.

But also, you might take a look at some existing projects in this 
general space that are already integrated with LLVM, such as Souper and 
Alive.

InstCombine is pretty cool but developing techniques to build these 
things automatically is awesome and on my wish list. There's potential 
for improvements in all of: speed, code quality, and correctness.

While we're on the subject: Are the canonicalization rules for LLVM IR 
documented anywhere?

Thanks,

John


https://github.com/google/souper
https://github.com/nunoplopes/alive



On 9/5/17 4:57 PM, (IIIT) Siddharth Bhat via llvm-dev
wrote:
> Hello all,
>
> I've seen some discussion that InstCombine is "too general"
and that
> llvm should implement a proper graph rewrite mechanism:
>
> Link to llvm-dev discussion about
> this: http://lists.llvm.org/pipermail/llvm-dev/2017-May/113219.html,
> Link to review where this came up (and I first heard about
> it): https://reviews.llvm.org/D37195.
>
> I wanted to understand what the current issues with InstCombine are, and
> if a graph rewriter prototype is something people are interested in. I
> find the idea appealing, from what little I know it, so I'd be
> interested in hacking something up.
>
> What would such a framework look like? Is there past literature on the
> subject? From what I know, many functional compilers using combinator
> based compilation were graph rewriting. Is there other prior art?
>
> Also, there is the idea of Equality Saturation
> (http://www.cs.cornell.edu/~ross/publications/eqsat/) that I found out
> about recently. Could this be used to augment the InstCombine
> infrastructure?
>
> Thanks,
> ~Siddharth
>
> --
> Sending this from my phone, please excuse any typos!
>
>
> _______________________________________________
> LLVM Developers mailing list
> llvm-dev at lists.llvm.org
> http://lists.llvm.org/cgi-bin/mailman/listinfo/llvm-dev
>

Thanks for the response.

Should I create a small prototype of equality saturation as an LLVM pass so
that there can be some concrete discussion on this? I'd love pointers.

Thanks,
Siddharth

On Wed 6 Sep, 2017, 23:35 John Regehr via llvm-dev <llvm-dev at
lists.llvm.org>
wrote:
> Equality saturation is very cool work and Ross Tate mentioned to me that
> he'd be happy to chat with you about this.
>
> But also, you might take a look at some existing projects in this
> general space that are already integrated with LLVM, such as Souper and
> Alive.
>
> InstCombine is pretty cool but developing techniques to build these
> things automatically is awesome and on my wish list. There's potential
> for improvements in all of: speed, code quality, and correctness.
>
> While we're on the subject: Are the canonicalization rules for LLVM IR
> documented anywhere?
>
> Thanks,
>
> John
>
>
> https://github.com/google/souper
> https://github.com/nunoplopes/alive
>
>
>
> On 9/5/17 4:57 PM, (IIIT) Siddharth Bhat via llvm-dev wrote:
> > Hello all,
> >
> > I've seen some discussion that InstCombine is "too
general" and that
> > llvm should implement a proper graph rewrite mechanism:
> >
> > Link to llvm-dev discussion about
> > this: http://lists.llvm.org/pipermail/llvm-dev/2017-May/113219.html,
> > Link to review where this came up (and I first heard about
> > it): https://reviews.llvm.org/D37195.
> >
> > I wanted to understand what the current issues with InstCombine are,
and
> > if a graph rewriter prototype is something people are interested in. I
> > find the idea appealing, from what little I know it, so I'd be
> > interested in hacking something up.
> >
> > What would such a framework look like? Is there past literature on the
> > subject? From what I know, many functional compilers using combinator
> > based compilation were graph rewriting. Is there other prior art?
> >
> > Also, there is the idea of Equality Saturation
> > (http://www.cs.cornell.edu/~ross/publications/eqsat/) that I found out
> > about recently. Could this be used to augment the InstCombine
> > infrastructure?
> >
> > Thanks,
> > ~Siddharth
> >
> > --
> > Sending this from my phone, please excuse any typos!
> >
> >
> > _______________________________________________
> > LLVM Developers mailing list
> > llvm-dev at lists.llvm.org
> > http://lists.llvm.org/cgi-bin/mailman/listinfo/llvm-dev
> >
> _______________________________________________
> LLVM Developers mailing list
> llvm-dev at lists.llvm.org
> http://lists.llvm.org/cgi-bin/mailman/listinfo/llvm-dev
>
-- 
Sending this from my phone, please excuse any typos!
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
<http://lists.llvm.org/pipermail/llvm-dev/attachments/20170907/bff5911c/attachment-0001.html>

On 09/05/2017 05:57 PM, (IIIT) Siddharth Bhat via llvm-dev wrote:
> Hello all,
>
> I've seen some discussion that InstCombine is "too general"
and that
> llvm should implement a proper graph rewrite mechanism:
>
> Link to llvm-dev discussion about this: 
> http://lists.llvm.org/pipermail/llvm-dev/2017-May/113219.html,
> Link to review where this came up (and I first heard about it): 
> https://reviews.llvm.org/D37195.
>
> I wanted to understand what the current issues with InstCombine are, 
> and if a graph rewriter prototype is something people are interested 
> in. I find the idea appealing, from what little I know it, so I'd be 
> interested in hacking something up.
>
> What would such a framework look like? Is there past literature on the 
> subject? From what I know, many functional compilers using combinator 
> based compilation were graph rewriting. Is there other prior art?
I'm not sure that I'd describe it as "too general", but I
suspect that
it could be made much more efficient. Currently, the patterns are 
implemented in C++, which is often fairly verbose, and because many of 
the checks are implemented separately, we end up touching instructions 
many times as we attempt to match different patterns. Worse, for many of 
these instructions we end up checking properties, such as known bits, 
that are computed by further backward instructions visiting. It is also 
hard to automatically check the correctness of the transformations, and 
moreover, it is hard to prove that we'll eventually reach a fixed point 
(we've certainly had problems in the past where some inputs would cause 
an endless loop between two different InstCombine patterns).

I'd love to see a solution where most of the transformations were 
specified in TableGen files and:
  1. We, as a result, had an easy way to convert these into a form where 
some SMT-solver-based checker could certify correctness.
  2. We, as a result, has an easy way to somehow check soundness, as a 
rewrite system, so we'd know it would reach a fixed point for all inputs.
  3. We, as a result, reduced the number of lines of code we need to 
maintain for these peephole optimizations.
  4. We, as a result, could generate efficient code for matching the 
patterns using some automaton technique for minimizing unnecessary 
visiting of instructions.

I'm not sure how closely it matches what we would need, but Stratego/XT 
comes to mind in terms of prior art (now here: 
http://www.metaborg.org/en/latest/). There's been a lot of work over the 
years on terminating graph rewriting systems in compilers.

  -Hal
>
> Also, there is the idea of Equality Saturation 
> (http://www.cs.cornell.edu/~ross/publications/eqsat/ 
> <http://www.cs.cornell.edu/%7Eross/publications/eqsat/>) that I found
> out about recently. Could this be used to augment the InstCombine 
> infrastructure?
>
> Thanks,
> ~Siddharth
>
> -- 
> Sending this from my phone, please excuse any typos!
>
>
> _______________________________________________
> LLVM Developers mailing list
> llvm-dev at lists.llvm.org
> http://lists.llvm.org/cgi-bin/mailman/listinfo/llvm-dev
-- 
Hal Finkel
Lead, Compiler Technology and Programming Languages
Leadership Computing Facility
Argonne National Laboratory

-------------- next part --------------
An HTML attachment was scrubbed...
URL:
<http://lists.llvm.org/pipermail/llvm-dev/attachments/20170908/cfec3a54/attachment.html>

> I'd love to see a solution where most of the transformations were 
> specified in TableGen files and:
>   1. We, as a result, had an easy way to convert these into a form where 
> some SMT-solver-based checker could certify correctness.
>   2. We, as a result, has an easy way to somehow check soundness, as a 
> rewrite system, so we'd know it would reach a fixed point for all
inputs.
>   3. We, as a result, reduced the number of lines of code we need to 
> maintain for these peephole optimizations.
>   4. We, as a result, could generate efficient code for matching the 
> patterns using some automaton technique for minimizing unnecessary 
> visiting of instructions.
YES to all of this (except TableGen :).

It should also be possible to find chains of transformations that fire 
in sequence and make them happen all at once, avoiding intermediate 
results and associated allocations/deallocations. Nuno has some ideas 
along these lines.
> I'm not sure how closely it matches what we would need, but Stratego/XT
> comes to mind in terms of prior art (now here: 
> http://www.metaborg.org/en/latest/). There's been a lot of work over
the
> years on terminating graph rewriting systems in compilers.
I went down this rabbit hole a few years ago, there's indeed a lot of 
existing material.

John

Hi,

On Tue, Sep 5, 2017 at 3:57 PM, (IIIT) Siddharth Bhat via llvm-dev <
llvm-dev at lists.llvm.org> wrote:
> Hello all,
>
> I've seen some discussion that InstCombine is "too general"
and that llvm
> should implement a proper graph rewrite mechanism:
>
> Link to llvm-dev discussion about this: http://lists.llvm.org/
> pipermail/llvm-dev/2017-May/113219.html,
> Link to review where this came up (and I first heard about it):
> https://reviews.llvm.org/D37195.
>
> I wanted to understand what the current issues with InstCombine are, and
> if a graph rewriter prototype is something people are interested in. I find
> the idea appealing, from what little I know it, so I'd be interested in
> hacking something up.
>
> What would such a framework look like? Is there past literature on the
> subject? From what I know, many functional compilers using combinator based
> compilation were graph rewriting. Is there other prior art?
>
> Also, there is the idea of Equality Saturation (
> http://www.cs.cornell.edu/~ross/publications/eqsat/) that I found out
> about recently. Could this be used to augment the InstCombine
> infrastructure?
>
In addition of augmenting InstCombine, we may also use Equality Saturation
to enhance/simplify the SCEV canonicalization process in the
ScalarEvolution pass, as well as the peephole optimizations in LLVM
backends.
So we may need a generic engine.


>
> Thanks,
> ~Siddharth
>
> --
> Sending this from my phone, please excuse any typos!
>
> _______________________________________________
> LLVM Developers mailing list
> llvm-dev at lists.llvm.org
> http://lists.llvm.org/cgi-bin/mailman/listinfo/llvm-dev
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
<http://lists.llvm.org/pipermail/llvm-dev/attachments/20170925/f55b665b/attachment.html>