3 ms·

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

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.

psi-squared 10y ago
(edited to add: Note that superoptimization isn't something you do to a whole program, it's more a thing you do to speed-critical sections of a larger program, ideally on the order of a few dozen instructions at most. That alone makes things a lot more tractable) (edit 2: I've read the relevant papers now, and have corrected some of the stuff below. Corrections are in italics.) The paper says that this system is built on top of STOKE, which uses the following verification method: * Generate a random set of test cases * Each intermediate code block gets instrumented and run on the host processor * The intermediate code block are given a cost depending on how different their results are from those of the original block on the current test set, as well as an estimate of the running time * If we get a code block which is correct on all the current test cases, we ask a theorem prover whether it's equivalent to the original one. If it isn't, the theorem prover spits out a test case which proves they're different, and we add that to the test set for future iterations. Finally, the fastest few provably-correct results are output, where they can be further tested in a full run of the original program they were taken from. The main room for error here is in the theorem proving step, which requires knowing the full semantics of the host's machine code. But it feels like that part should be share-able between different projects, as it's pretty much independent of the search method used.
chriswarbo 10y ago
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.
nickpsecurity 10y ago
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/ https://www.cis.upenn.edu/~stevez/vellvm/

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.

psi-squared 10y ago

(edited to add: Note that superoptimization isn't something you do to a whole program, it's more a thing you do to speed-critical sections of a larger program, ideally on the order of a few dozen instructions at most. That alone makes things a lot more tractable) (edit 2: I've read the relevant papers now, and have corrected some of the stuff below. Corrections are in italics.) The paper says that this system is built on top of STOKE, which uses the following verification method: * Generate a random set of test cases * Each intermediate code block gets instrumented and run on the host processor * The intermediate code block are given a cost depending on how different their results are from those of the original block on the current test set, as well as an estimate of the running time * If we get a code block which is correct on all the current test cases, we ask a theorem prover whether it's equivalent to the original one. If it isn't, the theorem prover spits out a test case which proves they're different, and we add that to the test set for future iterations. Finally, the fastest few provably-correct results are output, where they can be further tested in a full run of the original program they were taken from. The main room for error here is in the theorem proving step, which requires knowing the full semantics of the host's machine code. But it feels like that part should be share-able between different projects, as it's pretty much independent of the search method used.

chriswarbo 10y ago

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.

nickpsecurity 10y ago

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/ https://www.cis.upenn.edu/~stevez/vellvm/