This is the mail archive of the
mailing list for the GCC project.
Re: Speeding up compiled code with SAT
- From: Ian Lance Taylor <iant at google dot com>
- To: Mate Soos <mate at srlabs dot de>
- Cc: <gcc-help at gcc dot gnu dot org>
- Date: Fri, 15 Apr 2011 08:40:35 -0700
- Subject: Re: Speeding up compiled code with SAT
- References: <4DA84F8B.firstname.lastname@example.org>
Mate Soos <email@example.com> writes:
> This idea has been brewing in my head lately. Basically, when I think
> about the simplification steps that GCC does, it reminds me of applying
> algebraic tautologies to simplify equations. The problem with that is
> that there is no real reasoning involved, by which I mean that when a
> propagation of a truth is not possible any further, we put our hands in
> the air. SAT solvers go around this by guessing values, deriving
> conflicts, trying to resolve the problem using the DPLL algorithm --
> which is worst-case exponential of course, so it can be slow (but
> usually isn't).
> The point is that maybe we could try to use some real reasoning (not
> just fact propagation) on the internal representation that GCC builds
> from the code. This could be just a tech demo, and then later integrated
> into GCC as a plug-in to do e.g. final compilations of stuff like
> Firefox, where if the final compilation takes 1 CPU year, it's fine.
> This could allow us to do some really whacky automated reasoning to
> speed up complied code. Naturally, we would still need to limit the
> reasoning engine (by e.g. number of conflicts derived), and throw our
> hands in the air if nothing gets derived within that limit.
> I could come up with any number of possibilities how this would speed up
> compiled code, but I will save that to your imagination -- I am guessing
> you know much more about this part than me. I am just a SAT solver guy.
> Anyone thinks this may not be impossible? Or has this already been done?
It sounds like an idea which would be extremely expensive in compilation
time. Nobody will use a compiler which takes too long to compile.
We don't need to go as far as you suggest. For example, we could get
better register allocation we if put more time into it, by trying out
several different possibilities. That would be a fairly straightforward
change, almost certainly easier to implement than what you suggest. But
we don't do it, because it would take too long, so nobody would use it.
You can casually say that nobody cares if the final compilation of
firefox takes 1 CPU year, but in fact people do care, because they want
to test what they ship.
I don't want to discourage you from exploring this idea if you find it
interesting, but I'm pretty skeptical that it would ever become part of
a gcc distribution.