Elamur Research⌕
☰
home / papers / 2012 / Stochastic Superoptimization

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.

Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.

 Institutions

 Fields, topics and concepts

Cite

Cite as Eric Schkufza, Rahul Sharma and Alex Aiken. 2012. Stochastic Superoptimization. arXiv:1211.0557.

The paper itself, not this page. BibTeX from the library's record of the work. DOI 10.48550/arxiv.1211.0557 · 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

20 references, 1 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

  1. Markov Chain Monte Carlo in Practice: Interdisciplinary Statistics (Chapman & Hall/CRC Interdisciplinary Statistics). Chapman and Hall/CRC, 1 edition, Dec. 1995. find
  2. 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
  3. 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.
  4. 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
  5. 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
  6. S. Chenney and D. A. Forsyth. Sampling plausible solutions to multi-body constraint problems, 2000. find
  7. P. Diaconis. The Markov Chain Monte Carlo Revolution. Bulletin of the American Mathematical Society, 46(2):179–205, Nov. 2008. find
  8. V. Ganesh and D. L. Dill. A decision procedure for bit-vectors and arrays. In CAV, pages 519–531, 2007. find
  9. 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
  10. W. K. Hastings. Monte Carlo sampling methods using Markov chains and their applications. Biometrika, 57(1):97–109, Apr. 1970. find
  11. R. Joshi, G. Nelson, and K. H. Randall. Denali: A goal-directed superoptimizer. In PLDI, pages 304–314, 2002. find
  12. 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
  13. P. Liang, M. I. Jordan, and D. Klein. Learning programs: A hierarchical Bayesian approach. In International Conference on Machine Learning (ICML), 2010. find
  14. 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
  15. 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
  16. 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
  17. 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
  18. R. Tate, M. Stepp, Z. Tatlock, and S. Lerner. Equality saturation: a new approach to optimization. In POPL, 1 2009. find
  19. E. Veach and L. J. Guibas. Metropolis light transport. In Computer Graphics (SIGGRAPH ’97 Proceedings, pages 65–76. Addison Wesley, 1997. find
  20. H. S. Warren. Hacker’s Delight. Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA, 2002. find

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/schkufza-2012-stochastic-superoptimization/