More Web Proxy on the site http://driver.im/

research-article

Stochastic superoptimization

Authors:

Alex AikenAuthors Info & Claims

ACM SIGARCH Computer Architecture News, Volume 41, Issue 1

Pages 305 - 316

https://doi.org/10.1145/2490301.2451150

Published: 16 March 2013 Publication History

Abstract

We formulate the loop-free binary superoptimization task as a stochastic search problem. The competing constraints of transformation correctness and performance improvement are encoded as terms in a cost function, and a Markov Chain Monte Carlo sampler is used to rapidly explore the space of all possible programs to find one that is an optimization of a given target program. Although our method sacrifices completeness, the scope of programs we are able to consider, and the resulting quality of the programs that we produce, far exceed those of existing superoptimizers. Beginning from binaries compiled by llvm -O0 for 64-bit x86, our prototype implementation, STOKE, is able to produce programs which either match or outperform the code produced by gcc -O3, icc -O3, and in some cases, expert handwritten assembly.

References

[1]

C. Andrieu, N. de Freitas, A. Doucet, and M. I. Jordan. An introduction to MCMC for machine learning. Machine Learning, 50(1-2):5--43, 2003.

[2]

S. Bansal and A. Aiken. Automatic generation of peephole superoptimizers. In ASPLOS, pages 394--403, 2006.

Digital Library

[3]

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.

Digital Library

[4]

C. Cadar, D. Dunbar, and D. R. Engler. Klee: Unassisted and automatic generation of high-coverage tests for complex systems programs. In OSDI, pages 209--224, 2008.

Digital Library

[5]

S. Chenney and D. A. Forsyth. Sampling plausible solutions to multi-body constraint problems. In SIGGRAPH, pages 219--228, 2000.

Digital Library

[6]

P. Diaconis. The markov chain monte carlo revolution. Bulletin of the American Mathematical Society, 46(2):179--205, Nov. 2008.

[7]

V. Ganesh and D. L. Dill. A decision procedure for bit-vectors and arrays. In CAV, pages 519--531, 2007.

Digital Library

[8]

W. R. Gilks. Markov Chain Monte Carlo in Practice. Chapman and Hall/CRC, 1999.

[9]

S. Gulwani, S. Jha, A. Tiwari, and R. Venkatesan. Synthesis of loop-free programs. In PLDI, pages 62--73, 2011.

Digital Library

[10]

W. K. Hastings. Monte carlo sampling methods using markov chains and their applications. Biometrika, 57(1):97--109, Apr. 1970.

[11]

R. Joshi, G. Nelson, and K. H. Randall. Denali: A goal-directed superoptimizer. In PLDI, pages 304--314, 2002.

Digital Library

[12]

P. Liang, M. I. Jordan, and D. Klein. Learning programs: A hierarchical bayesian approach. In ICML, pages 639--646, 2010.

[13]

C.-K. Luk, R. S. Cohn, R. Muth, H. Patil, A. Klauser, P. G. Lowney, S. Wallace, V. J. Reddi, and K. M. Hazelwood. Pin: Building customized program analysis tools with dynamic instrumentation. In PLDI, pages 190--200, 2005.

Digital Library

[14]

H. Massalin. Superoptimizer - a look at the smallest program. In ASPLOS, pages 122--126, 1987.

Digital Library

[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.

[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.

[17]

A. Solar-Lezama, L. Tancau, R. Bodık, S. A. Seshia, and V. A. Saraswat. Combinatorial sketching for finite programs. In ASPLOS, pages 404--415, 2006.

Digital Library

[18]

R. Tate, M. Stepp, Z. Tatlock, and S. Lerner. Equality saturation: a new approach to optimization. In POPL, pages 264--276, 2009.

Digital Library

[19]

E. Veach and L. J. Guibas. Metropolis light transport. In SIGGRAPH, pages 65--76, 1997.

Digital Library

[20]

H. S. Warren. Hacker's Delight. Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA, 2002.

Digital Library

Cited By

Hong QAiken A(2024)Recursive Program Synthesis using ParamorphismsProceedings of the ACM on Programming Languages10.1145/36563818:PLDI(102-125)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656381
Shenoy APrabhu SMadhukar KShemer RSrivas M(2023)Automated Property Directed Self CompositionAutomated Technology for Verification and Analysis10.1007/978-3-031-45332-8_7(139-158)Online publication date: 24-Oct-2023
https://dl.acm.org/doi/10.1007/978-3-031-45332-8_7
Xu SGhosh BHobbs CFraccaroli EDuggirala PChakraborty S(2023)Statistical Approach to Efficient and Deterministic Schedule Synthesis for Cyber-Physical SystemsAutomated Technology for Verification and Analysis10.1007/978-3-031-45329-8_15(312-333)Online publication date: 24-Oct-2023
https://dl.acm.org/doi/10.1007/978-3-031-45329-8_15
Show More Cited By

Index Terms

Stochastic superoptimization
1. Software and its engineering
  1. Software notations and tools
    1. Compilers
2. Theory of computation
  1. Logic
    1. Logic and verification

Recommendations

Stochastic superoptimization
ASPLOS '13

We formulate the loop-free binary superoptimization task as a stochastic search problem. The competing constraints of transformation correctness and performance improvement are encoded as terms in a cost function, and a Markov Chain Monte Carlo sampler ...
Stochastic superoptimization
ASPLOS '13: Proceedings of the eighteenth international conference on Architectural support for programming languages and operating systems

We formulate the loop-free binary superoptimization task as a stochastic search problem. The competing constraints of transformation correctness and performance improvement are encoded as terms in a cost function, and a Markov Chain Monte Carlo sampler ...
Stochastic optimization of floating-point programs with tunable precision
PLDI '14: Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation

The aggressive optimization of floating-point computations is an important problem in high-performance computing. Unfortunately, floating-point instruction sets have complicated semantics that often force compilers to preserve programs as written. We ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGARCH Computer Architecture News

ACM SIGARCH Computer Architecture News Volume 41, Issue 1

ASPLOS '13

March 2013

540 pages

ISSN:0163-5964

DOI:10.1145/2490301

Issue’s Table of Contents

ASPLOS '13: Proceedings of the eighteenth international conference on Architectural support for programming languages and operating systems
March 2013
574 pages
ISBN:9781450318709
DOI:10.1145/2451116
General Chair:
Vivek Sarkar
Rice University, USA
,
Program Chair:
Rastislav Bodik
University of California, Berkeley, USA

Copyright © 2013 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 16 March 2013

Published in SIGARCH Volume 41, Issue 1

Check for updates

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

247
Total Citations
View Citations
1,559
Total Downloads

Downloads (Last 12 months)151
Downloads (Last 6 weeks)16

Reflects downloads up to 13 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Hong QAiken A(2024)Recursive Program Synthesis using ParamorphismsProceedings of the ACM on Programming Languages10.1145/36563818:PLDI(102-125)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656381
Shenoy APrabhu SMadhukar KShemer RSrivas M(2023)Automated Property Directed Self CompositionAutomated Technology for Verification and Analysis10.1007/978-3-031-45332-8_7(139-158)Online publication date: 24-Oct-2023
https://dl.acm.org/doi/10.1007/978-3-031-45332-8_7
Xu SGhosh BHobbs CFraccaroli EDuggirala PChakraborty S(2023)Statistical Approach to Efficient and Deterministic Schedule Synthesis for Cyber-Physical SystemsAutomated Technology for Verification and Analysis10.1007/978-3-031-45329-8_15(312-333)Online publication date: 24-Oct-2023
https://dl.acm.org/doi/10.1007/978-3-031-45329-8_15
Mell SBastani FZdancewic SBastani O(2023)Synthesizing Trajectory Queries from ExamplesComputer Aided Verification10.1007/978-3-031-37706-8_23(459-484)Online publication date: 17-Jul-2023
https://dl.acm.org/doi/10.1007/978-3-031-37706-8_23
Kolesar JPiskac RHallahan W(2022)Checking equivalence in a non-strict languageProceedings of the ACM on Programming Languages10.1145/35633406:OOPSLA2(1469-1496)Online publication date: 31-Oct-2022
https://dl.acm.org/doi/10.1145/3563340
Kang SKim JCho EChoi SRichard GBlazytko T(2022)Program Synthesis-based Simplification of MBA Obfuscated Malware with Restart StrategiesProceedings of the 2022 ACM Workshop on Research on offensive and defensive techniques in the context of Man At The End (MATE) attacks10.1145/3560831.3564258(13-18)Online publication date: 11-Nov-2022
https://dl.acm.org/doi/10.1145/3560831.3564258
Mammadli RSelakovic MWolf FPradel MSamanta RDillig I(2021)Learning to make compiler optimizations more effectiveProceedings of the 5th ACM SIGPLAN International Symposium on Machine Programming10.1145/3460945.3464952(9-20)Online publication date: 21-Jun-2021
https://dl.acm.org/doi/10.1145/3460945.3464952
Xu QWong MWagle TNarayana SSivaraman AKuipers FCaesar M(2021)Synthesizing safe and efficient kernel extensions for packet processingProceedings of the 2021 ACM SIGCOMM 2021 Conference10.1145/3452296.3472929(50-64)Online publication date: 9-Aug-2021
https://dl.acm.org/doi/10.1145/3452296.3472929
Zhang TChen ZZhu YVaithilingam PWang XGlassman EKitamura YQuigley AIsbister KIgarashi TBjørn PDrucker S(2021)Interpretable Program SynthesisProceedings of the 2021 CHI Conference on Human Factors in Computing Systems10.1145/3411764.3445646(1-16)Online publication date: 6-May-2021
https://dl.acm.org/doi/10.1145/3411764.3445646
Gupta KChristensen PChen XSong DLarochelle HRanzato MHadsell RBalcan MLin H(2020)Synthesize, execute and debugProceedings of the 34th International Conference on Neural Information Processing Systems10.5555/3495724.3497208(17685-17695)Online publication date: 6-Dec-2020
https://dl.acm.org/doi/10.5555/3495724.3497208
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents