Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Learning to Superoptimize Programs

arxiv.org

Post reply on HN
Print view View original

21–28 of 28 posts

Re: Learning to Superoptimize Programs

#21

Post by dom0 »

bloaf wrote: post #20
sanxiyn wrote: post #13

Earlier quoted context omitted.

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.

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.

Re: Learning to Superoptimize Programs

#22

Post by GFK_of_xmaspast »

cnkal wrote: post #11

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.

> In most real world scenarios there is no canonical objective function

How does this claim mesh with this quote from the paper: """Stoke (Schkufza et al., 2013) performs black-box optimization of a cost function on the space of programs, represented as a series of instructions. Each instruction is composed of an opcode, specifying what to execute, and some operands, specifying the corresponding registers. Each given input program T defines a cost function. For a candidate program R called rewrite, the goal is to optimize the following cost function"""

Re: Learning to Superoptimize Programs

#23

Post by nickpsecurity »

sanxiyn wrote: post #7

This 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…

That sounds pretty awesome. So, are these only instruction-level optimizations or is there a good toolkit for doing it SSA level as well? My idea being combining it with formal, equivalence checks in certified compilers so we get optimizations plus ensure correctness given original version was correct via certified transform. Certified to v1 -> superoptimize to v2 -> certified checker (v1, v2) -> rinse repeat.

Re: Learning to Superoptimize Programs

#24

Post by nickpsecurity »

coldcode wrote: post #9

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

We already have tools for proving applications and compilations correct. The problem is there's little to no optimization of those applications because optimizations can break correctness. One aspect of research like this is skirting that by throwing all kinds of optimizations at something combined with equivalence checks that ensure the new form is semantically equal to original form that we know was correct.

For example, CompCert compiler will produce correct assembly from a correct, C program. A set of optimizations might be available for the middle passes. Let's say C program gets taken to form I for intermediate. We know I is correct because that's what CompCert does. Applying J = optimize(I) might break it semantically in process of trying to speed it up. J might not equal I in some way. So, strategy is to develop an equivalence check as strong as CompCert to do J = Optimize(I), If Equals(I, J), Then Return J, Else Return I.

An example of a project doing this for real-world stuff is effort to formalize and equivalence-check LLVM's intermediate code:

https://www.cis.upenn.edu/~stevez/vellvm/

Re: Learning to Superoptimize Programs

#26

Post by nhaehnle »

sanxiyn wrote: post #13
bloaf wrote: post #12

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…

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

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.

Re: Learning to Superoptimize Programs

#27

Post by jfbastien »

nickpsecurity wrote: post #23
sanxiyn wrote: post #7

This 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…

That sounds pretty awesome. So, are these only instruction-level optimizations or is there a good toolkit for doing it SSA level as well? My idea being combining it with formal, equivalence checks in certified compilers so we get optimizations plus ensure correctness given original version was correct via certified transform. Certified to v1 -> superoptimize to v2 -> certified checker (v1, v2) -> rinse repeat.

souper: https://github.com/google/souper

Re: Learning to Superoptimize Programs

#28

Post by nickpsecurity »

jfbastien wrote: post #27
nickpsecurity wrote: post #23

Earlier quoted context omitted.

That sounds pretty awesome. So, are these only instruction-level optimizations or is there a good toolkit for doing it SSA level as well? My idea being combining it with formal, equivalence checks in certified compilers so we get optimizations plus ensure correctness given original version was correct via certified transform. Certified to v1 -> superoptimize to v2 -> certified checker (v1, v2) -> rinse repeat.

souper: https://github.com/google/souper

Hell yeah! Appreciate it.
Post reply on HN