Skip to content
The methodOpen data
Back to the collection

Souper: A Synthesizing Superoptimizer

Raimondas Sasnauskas, Yang Chen, Peter Collingbourne

Show all 7 authors

Jeroen Ketema, Gratian Lup, Jubi Taneja, John Regehr

2017 · arXiv

Programming languagesAlgorithms
Read the paper
HN score
0
Mentions
6
Readers
6
Months
5
What’s in a score?

From the abstract

If we can automatically derive compiler optimizations, we might be able to sidestep some of the substantial engineering challenges involved in creating and maintaining a high-quality compiler. We developed Souper, a synthesizing superoptimizer, to see how far these ideas might be pushed in the context of LLVM. Along the way, we discovered that Souper's intermediate representation was sufficiently similar to the one in Microsoft Visual C++ that we applied Souper to that compiler as well. Shipping, or about-to-ship, versions of both compilers contain optimizations suggested by Souper but implemented by hand. Alternately, when Souper is used as a fully automated optimization pass it compiles a Clang compiler binary that is about 3 MB (4.4%) smaller than the one compiled by LLVM.

Metadata: arXiv. Abstracts retain their original authors’ rights.

In the conversation

Original HN comments, with labels from simple text rules. A label describes the whole comment and may miss context or irony. Read the discussion to make up your own mind. About the labels

6 selected excerpts · 6 total mentions

muke101
Neutral mention · rule
If you're going to rewrite LLVM, you should avoid just trying to 'do it again but less bloated', because that'll end up where LLVM is now once you've added enough features and optimisation to be competitive. Rewriting LLVM gives you the opportunity to rethink some of its main problems. Of those I think two big ones include Tablegen and peephole optimisations. The backend code for LLVM is awful, and tablegen only partially addresses the problem. Most LLVM code for defining instruction opcodes amounts to multiple huge switch statements that stuff every opcode into them, its disgusting. This code is begging for a more elegant solution, I think a functional approach would…
Read the full comment
solve a lot of the problems. The peephole optimisation in the InstCombime pass is a huge collection of handwritten rules that's been accumulated over time. You probably don't want to try and redo this yourself but it will also be a big barrier to achieving competitive optimisation. You could try and solve the problem by using a superoprimisation approach from the beginning. Look into the Souper paper which automatically generates peepholes for LLVM: (https://github.com/google/souper, https://arxiv.org/pdf/1711.04422.pdf). Lastly as I hate C++ I have to throw in an obligatory suggestion to rewrite using Rust :p
Original comment Tilde, My LLVM Alternative
judofyr
Neutral mention · rule
But it has some kind of direct replacement mode, why aren't there benchmarks for that? Crickets... That's not fair. They've published a paper which has lots of details: https://arxiv.org/pdf/1711.04422.pdf > Performance of the SPEC benchmarks was also unevenly affected by Souper: five become faster and seven become slower. None of the differences was very large.
Original comment A Superoptimizer for LLVM IR
rahimiali
Neutral mention · rule
I'm not sure if I'm interpreting the paper [0] correctly, but both the abstract and the quote below from the Experiments section sound like they're not going to aim for faster code, but for a meta goal (that I admit I don't understand) instead? "The goal is to give compiler developers actionable advice about missing optimizations. To do this, someone uses sclang to extract Souper left-hand sides from programs of interest. Since Souper finds many more optimizations than developers could reasonably implement, the crux is ranking them in such a way that desirable optimizations are found early in the list. We are not aware of any single best ranking function, but rather we have created several such functions that can be used together or separately" [0] https://arxiv.org/abs/1711.04422
Original comment A Superoptimizer for LLVM IR
chrisaycock
Neutral mention · rule
Program synthesis [1] can be used for a variety of applications, including superoptimizers [2] and programming by example [3]. [1] https://dl.acm.org/citation.cfm?id=3208071 [2] https://arxiv.org/abs/1711.04422 [3] https://www.microsoft.com/en-us/research/wp-content/uploads/...
Original comment Syntax-Guided Synthesis
tom_mellior
Neutral mention · rule
Yes, if you use Z3 as part of a proof assistant like Isabelle/HOL or F-Star. No, if you use Z3 as part of some other system that does not have its own primitive notion of proofs and proof checking. Many tools are like this: Dafny is one, I think, as is Why3, and the Alive system for checking the correctness of LLVM peephole optimizations. They simply trust Z3. It's also used in lots of other things that are not "verifiers" as such. For example, to find new compiler optimizations by superoptimization: https://arxiv.org/abs/1711.04422 (And sure enough, if you search the paper for "Z3", the first hit is a paragraph where the authors describe that they once had a miscompilation due to a bug in Z3.)
Original comment Formal Verification: The Gap Between Perfect Code and Reality

Keep following the thread.

More in Programming languages

More from the same topics.