3 ms·

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 yo

• 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.