This technique is only as good as the objective function. In most real world scenarios there is no canonical objective function, nor a comprehensive test suite exercising all branches of the code.
Learning to Superoptimize Programs
11–20 of 28 posts
Re: Learning to Superoptimize Programs
#12As someone not well versed in compilers, this approach seems bizarre.
1. Given some chunk of a program, we should know ahead of time which I/O preserving transformations are available to us, because math.
2. Random search isn't going to find you some kind of Godel-esque situation where the optimized instructions are equivalent to the un-optimized ones in an unprovable way, especially when one of your steps is "prove equivalence."
So my question would be: why don't they just randomly apply I/O preserving transformations to the problem, skip the "output similarity" step, skip the theorem proving step, and just optimize against whatever actual performance benchmark they used?
Re: Learning to Superoptimize Programs
#13As someone not well versed in compilers, this approach seems bizarre. 1. Given some chunk of a program, we should know ahead of time which I/O preserving transformations are available to us, because math. 2. Random search isn't going to find you some kind of Godel-esque situation where the optimized instructions are equivalent to the un-optimized ones in an unprovable way, especially when one of your steps is "prove…
Because we "should", but actually don't, know ahead of time what semantic preserving transformations are available. The entire point is to discover them.
If you find this bizarre, consider that your semantic preserving transformations should be able to do examples in Figure 12 and 13 of http://theory.stanford.edu/~aiken/publications/papers/asplos...
Re: Learning to Superoptimize Programs
#14[deleted]
Re: Learning to Superoptimize Programs
#15This work should be read in context of prior work, STOKE: http://stoke.stanford.edu/ This work outperforms STOKE, and STOKE outperformed existing methods including GCC, LLVM, ICC, traditional superoptimization, expert human, etc. That's why comparison with existing methods are omitted. This work is also limited to Hacker's Delight and automatically generated programs, but so was STOKE. But STOKE readily extended to c…
[deleted]
Re: Learning to Superoptimize Programs
#16This technique is only as good as the objective function. In most real world scenarios there is no canonical objective function, nor a comprehensive test suite exercising all branches of the code.
While your point about objective function is correct, optimizing compilers still manage just fine with imperfect objective function, and superoptimizers do better. So "as good as objective function" is good enough.
This work proves functional equivalence, so no test suite is necessary.
Re: Learning to Superoptimize Programs
#17This technique is only as good as the objective function. In most real world scenarios there is no canonical objective function, nor a comprehensive test suite exercising all branches of the code.
While your point about objective function is correct, optimizing compilers still manage just fine with imperfect objective function, and superoptimizers do better. So "as good as objective function" is good enough. This work proves functional equivalence, so no test suite is necessary.
> optimizing compilers still manage just fine with imperfect objective function,
Imperfect or not, optimizing compilers do not require an objective function at all. The majority of computer programs do not have an objective function.
Re: Learning to Superoptimize Programs
#18[deleted]
Re: Learning to Superoptimize Programs
#19Even if this was useful, it presumes the ability to prove a application correct while modifying it. This would only be doable in very limited circumstances not general purpose applications.
You don't need to prove the application correct, you just have to prove the optimisation correct, i.e. that the generated code has the same observable behaviour as the given code, except for its resource usage.
Superoptimisation is an implementation detail, in the same way that existing compiler optimisations, JIT compilers, CPU branch predictors, etc. are optimisation details. The machine will behave according to the code you wrote, whether that code is correct or not.
Re: Learning to Superoptimize Programs
#20As someone not well versed in compilers, this approach seems bizarre. 1. Given some chunk of a program, we should know ahead of time which I/O preserving transformations are available to us, because math. 2. Random search isn't going to find you some kind of Godel-esque situation where the optimized instructions are equivalent to the un-optimized ones in an unprovable way, especially when one of your steps is "prove…
Because we "should", but actually don't, know ahead of time what semantic preserving transformations are available. The entire point is to discover them. If you find this bizarre, consider that your semantic preserving transformations should be able to do examples in Figure 12 and 13 of http://theory.stanford.edu/~aiken/publications/papers/asplos...
But it seems to me that the fact that they have a theorem prover at all means they do know ahead of time what semantic preserving transformations are available.