Stochastic Superoptimization
Paper · 2012 · Eric Schkufza, Rahul Sharma and Alex Aiken
Summary
Superoptimizers aim to find the fastest program equivalent to a given piece of code. Earlier systems searched exhaustively, which ensured completeness but restricted them to very short sequences, small opcode sets, or hand-written rewrite rules. Schkufza, Sharma and Aiken instead treat loop-free binary superoptimization as an incomplete, randomized search. They define a cost function with two parts: a correctness term that is zero only when a candidate behaves identically to the target on its live outputs, and a performance term that rewards faster code. A Markov Chain Monte Carlo sampler explores the very irregular space of 64-bit X86 instruction sequences to find low-cost rewrites. Candidates are first screened on testcases and then checked by a verifier. Their prototype, STOKE, starts from binaries produced by llvm -O0. On benchmarks from cryptography, linear algebra and low-level programming, it matches or beats gcc with full optimization, and occasionally expert hand-written assembly. Giving up completeness lets STOKE handle far longer programs and a much larger instruction set than previous superoptimizers.
Key points
- On the OpenSSL Montgomery multiplication kernel, STOKE started from a 116-line llvm -O0 binary and produced an 11-instruction rewrite. This rewrite is 16 lines shorter than gcc -O3 output, 1.6x faster, and slightly faster than OpenSSL's hand-written assembly. Its equivalence to the original was formally verified.
- STOKE's search covers much of the 64-bit X86 instruction set, which contains close to 400 opcodes. Massalin's superoptimizer handled sequences up to length 12 but only with 10–15 opcodes. Bansal's system was limited to inputs of length 6 or less and outputs of length 3 or less.
- On the SAXPY benchmark from BLAS (manually unrolled four times), STOKE found an SSE vectorized version. gcc -O3 did not produce it.
- The approach covers only loop-free code. Future work targets loops and a more robust synthesis cost function.
Institutions
Fields, topics and concepts
📚 Shelves 3The field of science this work belongs to (OpenAlex fields).Computer Science · 19,503 worksArtificial Intelligence · 18,805 worksHardware and Architecture · 183 works
Cite
Cite as Eric Schkufza, Rahul Sharma and Alex Aiken. 2012. Stochastic Superoptimization. arXiv:1211.0557.
@misc{schkufza2012stochastic,
title = {{Stochastic Superoptimization}},
author = {Eric Schkufza, Rahul Sharma and Alex Aiken},
year = {2012},
doi = {10.48550/arxiv.1211.0557},
eprint = {1211.0557},
archivePrefix = {arXiv},
url = {https://doi.org/10.48550/arxiv.1211.0557}
}References
- Markov Chain Monte Carlo in Practice: Interdisciplinary Statistics (Chapman & Hall/CRC Interdisciplinary Statistics). Chapman and Hall/CRC, 1 edition, Dec. 1995. find
- C. Andrieu, N. de Freitas, A. Doucet, and M. I. Jordan. An Introduction to MCMC for Machine Learning. Machine Learning, 50(1):5–43, Jan. 2003. find
- S. Bansal and A. Aiken. Automatic generation of peephole superoptimizers. In Proceedings of the 12th international conference on Architectural support for programming languages and operating systems, ASPLOS-XII, pages 394–403, New York, NY, USA, 2006. ACM.
- L. S. Blackford, J. Demmel, J. Dongarra, I. Duff, S. Hammarling, G. Henry, M. Heroux, L. Kaufman, A. Lumsdaine, A. Petitet, R. Pozo, K. Remington, and R. C. Whaley. An updated set of basic linear algebra subprograms (blas). ACM Transactions on Mathematical Software, 28:135–151, 2001. find
- C. Cadar, D. Dunbar, and D. Engler. Klee: Unassisted and automatic generation of high-coverage tests for complex systems programs. In Proceedings of the 8th USENIX conference on Operating systems design and implementation, OSDI’08, pages 209–224, Berkeley, CA, USA, 2008. USENIX Association. find
- S. Chenney and D. A. Forsyth. Sampling plausible solutions to multi-body constraint problems, 2000. find
- P. Diaconis. The Markov Chain Monte Carlo Revolution. Bulletin of the American Mathematical Society, 46(2):179–205, Nov. 2008. find
- V. Ganesh and D. L. Dill. A decision procedure for bit-vectors and arrays. In CAV, pages 519–531, 2007. find
- S. Gulwani, S. Jha, A. Tiwari, and R. Venkatesan. Synthesis of loop-free programs. In Proceedings of the 32nd ACM SIGPLAN conference on Programming language design and implementation, PLDI ’11, pages 62–73, New York, NY, USA, 2011. ACM. find
- W. K. Hastings. Monte Carlo sampling methods using Markov chains and their applications. Biometrika, 57(1):97–109, Apr. 1970. find
- R. Joshi, G. Nelson, and K. H. Randall. Denali: A goal-directed superoptimizer. In PLDI, pages 304–314, 2002. find
- C. keung Luk, R. Cohn, R. Muth, H. Patil, A. Klauser, G. Lowney, S. Wallace, V. Janapa, and R. K. Hazelwood. Pin: Building customized program analysis tools with dynamic instrumentation. In In Programming Language Design and Implementation, pages 190–200. ACM Press, 2005. find
- P. Liang, M. I. Jordan, and D. Klein. Learning programs: A hierarchical Bayesian approach. In International Conference on Machine Learning (ICML), 2010. find
- H. Massalin. Superoptimizer: a look at the smallest program. In Proceedings of the second international conference on Architectual support for programming languages and operating systems, ASPLOS-II, pages 122–126, Los Alamitos, CA, USA, 1987. IEEE Computer Society Press. find
- N. Metropolis, A. W. Rosenbluth, M. N. Rosenbluth, A. H. Teller, and E. Teller. Equation of State Calculations by Fast Computing Machines. The Journal of Chemical Physics, 21(6):1087–1092, 1953. find
- A. F. Neuwald, J. S. Liu, D. J. Lipman, and C. E. Lawrence. Extracting protein alignment models from the sequence database. Nucleic Acids Research, 25:1665–1677, 1997. find
- O. Solar-lezama, L. Tancau, R. Bodik, V. Saraswat, and S. Seshia. Combinatorial sketching for finite programs. In In 12th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS 2006, pages 404–415. ACM Press, 2006. find
- R. Tate, M. Stepp, Z. Tatlock, and S. Lerner. Equality saturation: a new approach to optimization. In POPL, 1 2009. find
- E. Veach and L. J. Guibas. Metropolis light transport. In Computer Graphics (SIGGRAPH ’97 Proceedings, pages 65–76. Addison Wesley, 1997. find
- H. S. Warren. Hacker’s Delight. Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA, 2002. find
Updated
This page in Markdown → https://md.research.elamur.ai/free/en/papers/schkufza-2012-stochastic-superoptimization/