4 ms·

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 algor

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