3 ms·

As 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 trans

by bloaf 10y ago

As 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?

sanxiyn 10y ago
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/asplos13.pdf http://theory.stanford.edu/~aiken/publications/papers/asplos...
- bloaf 10y ago
  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.
  - dom0 10y ago
    No. They have a verificator that can show that two (sub-)programs (more accurately; that an applied transformation preserves semantics) are semantically identical. This is a bit like a P-verificator for the solution to a NP-hard problem using a certificate. It can only help you prove that the solution is right, not find new solutions.
- nhaehnle 10y ago
  Ugh, the code in Figure 13 is mis-compiled by the super-optimizer. It seems that their checking procedure is flawed. How was that not caught in peer-review? The problem is that the ranges pointed by x and y could (partially) overlap, in which case the SSE-based optimization is incorrect. Edit: Even more damning, gcc actually does produce an equivalent optimal code sequence for me when the incoming pointers are correctly marked as restrict and -march=native is used. (Although perhaps that's due to different gcc versions; maybe a gcc improvement was inspired by that article.) Edit #2: I see they actually discuss this in the main article text. Oh well, I'm leaving the comment here since the figure by itself is misleading.

by bloaf 10y ago

sanxiyn 10y ago

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/asplos13.pdf http://theory.stanford.edu/~aiken/publications/papers/asplos...

bloaf 10y ago
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.
- dom0 10y ago
  No. They have a verificator that can show that two (sub-)programs (more accurately; that an applied transformation preserves semantics) are semantically identical. This is a bit like a P-verificator for the solution to a NP-hard problem using a certificate. It can only help you prove that the solution is right, not find new solutions.
nhaehnle 10y ago
Ugh, the code in Figure 13 is mis-compiled by the super-optimizer. It seems that their checking procedure is flawed. How was that not caught in peer-review? The problem is that the ranges pointed by x and y could (partially) overlap, in which case the SSE-based optimization is incorrect. Edit: Even more damning, gcc actually does produce an equivalent optimal code sequence for me when the incoming pointers are correctly marked as restrict and -march=native is used. (Although perhaps that's due to different gcc versions; maybe a gcc improvement was inspired by that article.) Edit #2: I see they actually discuss this in the main article text. Oh well, I'm leaving the comment here since the figure by itself is misleading.