48 ms·

How do you reason about correctness when stoke changes your code? Does it rely on invariance of test cases or does it try to 'understand' the intent of the prog

How do you reason about correctness when stoke changes your code? Does it rely on invariance of test cases or does it try to 'understand' the intent of the program?

radarsat1 6y ago
I guess this is what the second paragraph is about. "In addition to searching over programs, STOKE contains verification infrastructure to show the equivalence between x86-64 programs. STOKE can consider test-cases, perform bounded verification all the way to fully formal verification that shows the equivalence for all possible inputs."
- _hl_ 6y ago
  Program equivalence is in general uncomputable if I'm not mistaken, so a big part of the possible performance enhancements depend on the strength of their algorithm for proving equivalence. Definitely an interesting though extremely challenging problem.
  - GregarianChild 6y ago
    Undecidability of program equivalence only means that there is no algorithm that correctly returns the correct answer to the question P = Q? for ALL programs P, Q in a Turing-complete programming language. The original STOKE paper [1] only worked for loop free programs, which may be a program fragment for which program equivalence is decidable. Be that as it may, there is a fast heuristic for proving non-equivalence between two programs P and Q, just feed them with random input -- if they return different outputs, they are NOT equivalent, if OTOH they return the same results, they they are candidates for equivalence and you can throw a modern SMT solver at them which may actually be able to prove equivalence (or come up with a counterexample). Otherwise the SMT solver times out. You can even refine this scheme into some form of local search, in that you measure how much P and Q differ (e.g. Hamming distance). This is used in later papers, e.g. [2]. [1] Stochastic Superoptimization – ASPLOS 2013 https://raw.githubusercontent.com/StanfordPL/stoke/develop/docs/papers/asplos13.pdf https://raw.githubusercontent.com/StanfordPL/stoke/develop/d... [2] Stochastic Program Optimization – CACM 2016 https://raw.githubusercontent.com/StanfordPL/stoke/develop/docs/papers/cacm16.pdf https://raw.githubusercontent.com/StanfordPL/stoke/develop/d...
    - jonnypotty 6y ago
      Thanks for this
    - GTP 6y ago
      Thanks, I was looking for this explanation.
sanxiyn 6y ago
STOKE proves full equivalence.
- TheOtherHobbes 6y ago
  Of trivial code blocks. That's not a terrible goal if you want to make key libraries faster and more efficient. But I'm unconvinced that it would be easy to scale up these techniques to auto-clone and improve a big application like Photoshop or Word - or even a generic CRUD app.
  - naasking 6y ago
    Even big applications are composed of trivial code blocks. The optimisations are probably synergistic with other passes, and would probably expose many inlining opportunities that didn't exist before.
  - jcranmer 6y ago
    This is basically doing what compiler engineers call peephole optimization: optimizing small windows of code, which is a standard part of the optimizer pipeline. One advantage of peephole optimization is that pretty much all code is amenable to it, so it doesn't rely on their being one key, hot loop to optimize to see performance gains. The main disadvantage is that gains in peephole optimization tend to be quite small, so you're combing for single-digit percentage speedups.

How do you reason about correctness when stoke changes your code? Does it rely on invariance of test cases or does it try to 'understand' the intent of the program?

radarsat1 6y ago

I guess this is what the second paragraph is about. "In addition to searching over programs, STOKE contains verification infrastructure to show the equivalence between x86-64 programs. STOKE can consider test-cases, perform bounded verification all the way to fully formal verification that shows the equivalence for all possible inputs."

_hl_ 6y ago
Program equivalence is in general uncomputable if I'm not mistaken, so a big part of the possible performance enhancements depend on the strength of their algorithm for proving equivalence. Definitely an interesting though extremely challenging problem.
- GregarianChild 6y ago
  Undecidability of program equivalence only means that there is no algorithm that correctly returns the correct answer to the question P = Q? for ALL programs P, Q in a Turing-complete programming language. The original STOKE paper [1] only worked for loop free programs, which may be a program fragment for which program equivalence is decidable. Be that as it may, there is a fast heuristic for proving non-equivalence between two programs P and Q, just feed them with random input -- if they return different outputs, they are NOT equivalent, if OTOH they return the same results, they they are candidates for equivalence and you can throw a modern SMT solver at them which may actually be able to prove equivalence (or come up with a counterexample). Otherwise the SMT solver times out. You can even refine this scheme into some form of local search, in that you measure how much P and Q differ (e.g. Hamming distance). This is used in later papers, e.g. [2]. [1] Stochastic Superoptimization – ASPLOS 2013 https://raw.githubusercontent.com/StanfordPL/stoke/develop/docs/papers/asplos13.pdf https://raw.githubusercontent.com/StanfordPL/stoke/develop/d... [2] Stochastic Program Optimization – CACM 2016 https://raw.githubusercontent.com/StanfordPL/stoke/develop/docs/papers/cacm16.pdf https://raw.githubusercontent.com/StanfordPL/stoke/develop/d...
  - jonnypotty 6y ago
    Thanks for this
  - GTP 6y ago
    Thanks, I was looking for this explanation.

sanxiyn 6y ago

STOKE proves full equivalence.

TheOtherHobbes 6y ago
Of trivial code blocks. That's not a terrible goal if you want to make key libraries faster and more efficient. But I'm unconvinced that it would be easy to scale up these techniques to auto-clone and improve a big application like Photoshop or Word - or even a generic CRUD app.
- naasking 6y ago
  Even big applications are composed of trivial code blocks. The optimisations are probably synergistic with other passes, and would probably expose many inlining opportunities that didn't exist before.
- jcranmer 6y ago
  This is basically doing what compiler engineers call peephole optimization: optimizing small windows of code, which is a standard part of the optimizer pipeline. One advantage of peephole optimization is that pretty much all code is amenable to it, so it doesn't rely on their being one key, hot loop to optimize to see performance gains. The main disadvantage is that gains in peephole optimization tend to be quite small, so you're combing for single-digit percentage speedups.