Abstract: “Developing a code optimizer is challenging, especially for new, idiosyncratic ISAs. Superoptimization can, in principle, discover machine-specific optimizations automatically by searching the space of all instruction sequences. If we can increase the size of code fragments a superoptimizer can optimize, we will be able to discover more optimizations.
We develop LENS, a search algorithm that increases the size of code a superoptimizer can synthesize by rapidly pruning away invalid candidate programs. Pruning is achieved by selectively refining the abstraction under which candidates are considered equivalent, only in the promising part of the candidate space. LENS also uses a bidirectional search strategy to prune the candidate space from both forward and backward directions. These pruning strategies allow LENS to solve twice as many benchmarks as existing enumerative search algorithms, while LENS is about 11-times faster. Additionally, we increase the effective size of the superoptimized fragments by relaxing the correctness condition using contexts (surrounding code).
Finally, we combine LENS with complementary search techniques into a cooperative superoptimizer, which exploits the stochastic search to make random jumps in a large candidate space, and a symbolic (SAT-solver-based) search to synthesize arbitrary constants. While existing superoptimizers consistently solve 9–16 out of 32 benchmarks, the cooperative superoptimizer solves 29 benchmarks. It can synthesize code fragments that are up to 82% faster than code generated by gcc -O3 from WiBench and MiBench.”
Neat. Greenthumb on GitHub: https://github.com/mangpo/greenthumb
Coincidentally, I was re-watching Emina Torlak’s talks on Rosette yesterday :)
Here’s another cool application of Rosette, by the main author of this paper:
The Hint Generation paper looks like it’s worth its own submission. People might like it. You should submit it with the video in the text field.
Edit: And thanks for the other links, too. :)
Thanks for the suggestion; done: https://lobste.rs/s/rro40w/high_coverage_hint_generation_for
Previous discussion on Rosette (also submitted by nick):
https://lobste.rs/s/upoeur/rosetta_solver_aided_programming
P.S. No problems :)