Mate Soos <mate@xxxxxxxxx> 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. Ian
