u/wtbwin r/ReverseEngineering • Recommends
Stochastic Optimization for x86 Binaries (Google Tech Talk)
0:00 / 0:00
#stochasticoptimization#x86#mcmc
Stochastic Optimization for x86 Binaries
Google TechTalks
349K subscribers • 62 videos on Hallway
- Recommended by 1 person: 1 in engineering communities.
- Linked in the descriptioneschkufz/stoke-release
Advanced. Deep dive for people who know the field.
14K views11 years ago1 recommendation
Systems programmingProgramming languagesCompilers and interpretersPerformance and optimizationAlgorithms
How to use Markov Chain Monte Carlo sampling to generate aggressively optimized, provably correct x86 assembly sequences.
Google Tech Talks January 12, 2015 (more info below) ABSTRACT The optimization of short sequences of loop-free fixed-point x86_64 code sequences is an important problem in high-performance computing. Unfortunately, the competing constraints of transformation correctness and performance improvement often force even special purpose compilers to produce sub-optimal code. We show that by encoding these constraints as terms in a cost function, and using a Markov Chain Monte Carlo sampler to rapidly explore the space of all possible programs, we are able to generate aggressively optimized versions of a given target program. Beginning from binaries compiled by gcc -O0, we are able to produce provably correct code sequences that either match or outperform the code produced by gcc -O3, and in some cases expert hand-written assembly. Because most high-performance applications contain floating-point computations, we extend our technique to this domain and show a novel approach to trading full floating-point precision for further increases in performance. We demonstrate the ability to generate reduced precision implementations of Intel's handwritten C numerics library that are up to six times faster than the original code, and achieve end-to-end speedups of over 30% on a direct numeric simulation and a ray tracer. Because optimizations that contain floating-point computations are not amenable to formal verification using the state of the art, we present a technique for characterizing maximum error and providing strong evidence for correctness. Publication list: cs.stanford.edu/people/eschkufz/ Github: github.com/eschkufz/stoke-release About the speaker Eric Schkufza is a postdoctoral scholar at Stanford University working with professor Alex Aiken. He graduated from Stanford University with a PhD in computer science in June 2014. He is interested in applying stochastic search techniques to the design of optimizing compilers.Why it's here
1 person recommends thisu/PL_DesignAYYin r/ProgrammingLanguages • Mentions
On “Is there an automatic approach to program optimization?”
Yes, this exists. I don't know how effective it is outside of the examples they provide, but watch this video: link to this video
A notable limitation of this technique is that, excepting the weird stuff they're doing with floating point values, it cannot superoptimize any snippet of code that cannot be proven equivalent to some other snippet of code. From a theoretical PoV this is equivalent to solving the halting problem in the general case, but fortunately you do not need to solve it in the general case to get useful optimizations. From a practical PoV if you write code that cannot be proven equivalent to some other code with a SAT solver, then you're probably shit out of luck. I can't really rigor…
u/PL_DesignAYYin r/ProgrammingLanguages • Mentions
On “Lessons learned over the years.”
Right now we're using LLVM, but we have plans to write our own experimental x86-64 back end that uses super optimizing techniques for release builds. We want to do it this way so we don't need to deal with the complexities of undefined behavior or making sure we're applying transformation rules correctly. See:
https://kristerw.blogspot.com/2017/09/why-undefined-behavior-may-call-never.html
https://www.ralfj.de/blog/2020/12/14/provenance.html
link to this video
u/PL_Designin r/ProgrammingLanguages • Mentions
On “State of the Field and Setting Expectations”
An interesting option is to build a superoptimizer that uses a SAT/SMT solver to verify the correctness of its optimizations. Take a look at this: link to this video
What's notable here is that, presuming debug builds and release builds are equivalent, only debug builds generally need to compile quickly. Who cares if it takes a release build a week to optimize to the point of diminishing returns? Additionally, you can have a superoptimizer like this running on your most recent commits and caching useful optimizations it finds so it can optimize a release build quickly later on. You can have the superoptimizsr study your project as you build it.
An approach like this reduces the design space down to d…