HackerPapers

arXiv:1711.04422cs.PL

Souper: A Synthesizing Superoptimizer

Raimondas Sasnauskas, Yang Chen, Peter Collingbourne, Jeroen Ketema, Gratian Lup, Jubi Taneja, John Regehr

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.

arXiv comments
Journal reference
DOI
Subjects
cs.PLProgramming Languages

On Hacker News

Linked by 7 identifiable commenters in 7 comments across 6 threads, from Dec 2017 to Jul 2025. Found in 2 HN submissions from Nov 2017 to Nov 2017. Open submission discussions.

Comments linking this paper, per year.

Discussed in comments6 threads

  1. FFmpeg devs boast of another 100x leap thanks to handwritten assembly code 1 comment

    • You're missing forest for the trees and lacking information to discuss this really. Check out this paper and similar ones if you want to learn about this area: https://arxiv.org/pdf/1711.04422

      viraptorView on HNParent context

  2. Tilde, My LLVM Alternative 1 comment

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

      muke101View on HNParent context

  3. A Superoptimizer for LLVM IR 2 comments

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

      rahimialiView on HNParent context

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

      judofyrView on HNParent context

  4. Software Verification and Analysis Using Z3 1 comment
  5. Syntax-Guided Synthesis 1 comment

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

      chrisaycockView on HNParent context

  6. Formal Verification: The Gap Between Perfect Code and Reality 1 comment

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

      tom_melliorView on HNParent context

Submitted to Hacker News

Connected through shared HN threads, not inferred similarity or a recommendation.