5 ms·

Have you guys looked the literature of supercompilation? This seems to be a special case of it.

by rowanG077 5y ago

carlopi 5y ago
Hi, author of the post here, I am not familiar with this concept, do you have any pointers?
- rowanG077 5y ago
  The idea is to evaluate the program at compile time and obtain a trace of the program that allows you to reconstruct a semantically equivalent program which has some desirable properties. In your case (and most cases in literature) it's done for optimization. Partial evaluation, which is a subset of supercompilation, is similar to what you are doing. See the wiki page: https://en.wikipedia.org/wiki/Partial_evaluation https://en.wikipedia.org/wiki/Partial_evaluation Some literature: https://dl.acm.org/doi/10.1145/5956.5957 https://dl.acm.org/doi/10.1145/5956.5957 https://ndmitchell.com/downloads/paper-rethinking_supercompilation-29_sep_2010.pdf https://ndmitchell.com/downloads/paper-rethinking_supercompi...
moralestapia 5y ago
Supercompilation came to my mind as well! Wasm + SC would be a killer deal.
fulafel 5y ago
All analytical solutions to optimization problems can be seen as special cases of the brute force search I guess. But SC is impractically slow for anything except a few instructions long sequences. edit: actually I was thinking of superoptimizers, I guess it's a different concept.
- rowanG077 5y ago
  Supercompilation is not brute force search.
- titzer 5y ago
  Superoptimizers have gotten a lot better in the past few years. E.g. have a look at [1]. [1] https://arxiv.org/abs/1211.0557 https://arxiv.org/abs/1211.0557
  - fulafel 5y ago
    Thanks, cool stuff. This paper from the same project was also cool: https://raw.githubusercontent.com/StanfordPL/stoke/develop/docs/papers/oopsla15a.pdf https://raw.githubusercontent.com/StanfordPL/stoke/develop/d... Quote from abstract: " For many applications, the best possible code is conditionally correct: the optimized kernel is equal to the code that it replaces only under certain preconditions on the kernel’s inputs. The main technical challenge in producing conditionally correct opti- mizations is in obtaining non-trivial and useful conditions and proving conditional equivalence formally in the pres- ence of loops. We combine abstract interpretation, decision procedures, and testing to yield a verification strategy that can address both of these problems. This approach yields a superoptimizer for x86 that in our experiments produces binaries that are often multiple times faster than those pro- duced by production compilers"

Have you guys looked the literature of supercompilation? This seems to be a special case of it.

carlopi 5y ago

Hi, author of the post here, I am not familiar with this concept, do you have any pointers?

rowanG077 5y ago
The idea is to evaluate the program at compile time and obtain a trace of the program that allows you to reconstruct a semantically equivalent program which has some desirable properties. In your case (and most cases in literature) it's done for optimization. Partial evaluation, which is a subset of supercompilation, is similar to what you are doing. See the wiki page: https://en.wikipedia.org/wiki/Partial_evaluation https://en.wikipedia.org/wiki/Partial_evaluation Some literature: https://dl.acm.org/doi/10.1145/5956.5957 https://dl.acm.org/doi/10.1145/5956.5957 https://ndmitchell.com/downloads/paper-rethinking_supercompilation-29_sep_2010.pdf https://ndmitchell.com/downloads/paper-rethinking_supercompi...

moralestapia 5y ago

Supercompilation came to my mind as well! Wasm + SC would be a killer deal.

fulafel 5y ago

All analytical solutions to optimization problems can be seen as special cases of the brute force search I guess. But SC is impractically slow for anything except a few instructions long sequences. edit: actually I was thinking of superoptimizers, I guess it's a different concept.

rowanG077 5y ago
Supercompilation is not brute force search.
titzer 5y ago
Superoptimizers have gotten a lot better in the past few years. E.g. have a look at [1]. [1] https://arxiv.org/abs/1211.0557 https://arxiv.org/abs/1211.0557
- fulafel 5y ago
  Thanks, cool stuff. This paper from the same project was also cool: https://raw.githubusercontent.com/StanfordPL/stoke/develop/docs/papers/oopsla15a.pdf https://raw.githubusercontent.com/StanfordPL/stoke/develop/d... Quote from abstract: " For many applications, the best possible code is conditionally correct: the optimized kernel is equal to the code that it replaces only under certain preconditions on the kernel’s inputs. The main technical challenge in producing conditionally correct opti- mizations is in obtaining non-trivial and useful conditions and proving conditional equivalence formally in the pres- ence of loops. We combine abstract interpretation, decision procedures, and testing to yield a verification strategy that can address both of these problems. This approach yields a superoptimizer for x86 that in our experiments produces binaries that are often multiple times faster than those pro- duced by production compilers"