research-article

Generating compiler optimizations from proofs

Authors:

Sorin LernerAuthors Info & Claims

POPL '10: Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Pages 389 - 402

https://doi.org/10.1145/1706299.1706345

Published: 17 January 2010 Publication History

Abstract

We present an automated technique for generating compiler optimizations from examples of concrete programs before and after improvements have been made to them. The key technical insight of our technique is that a proof of equivalence between the original and transformed concrete programs informs us which aspects of the programs are important and which can be discarded. Our technique therefore uses these proofs, which can be produced by translation validation or a proof-carrying compiler, as a guide to generalize the original and transformed programs into broadly applicable optimization rules.

We present a category-theoretic formalization of our proof generalization technique. This abstraction makes our technique applicable to logics besides our own. In particular, we demonstrate how our technique can also be used to learn query optimizations for relational databases or to aid programmers in debugging type errors.

Finally, we show experimentally that our technique enables programmers to train a compiler with application-specific optimizations by providing concrete examples of original programs and the desired transformed programs. We also show how it enables a compiler to learn efficient-to-run optimizations from expensive-to-run super-optimizers.

References

[1]

J. Adámek, H. Herrlich, and G.E. Strecker. Abstract and Concrete Categories: The Joy of Cats. John Wiley & Sons, 1990.

Digital Library

[2]

S. Bansal and A. Aiken. Automatic generation of peephole superoptimizers. In ASPLOS, 2006.

Digital Library

[3]

R. Bergmann. Explanation-based learning for the automated reuse of programs. In CompEuro, 1992.

[4]

K.D. Cooper, D. Subramanian, and L. Torczon. Adaptive optimizing compilers for the 21st century. The Journal of Supercomputing, 23(1):7--22, Aug. 2002.

Digital Library

[5]

A. Deutsch. Author of {6}. Personal communication, July 2009.

[6]

A. Deutsch, A. Nash, and J. Remmel. The chase revisited. In PODS, 2008.

Digital Library

[7]

S. Dietzen and F. Pfenning. Higher-order and modal logic as a framework for explanation-based generalization. Machine Learning, 9(1):23--55, June 1992.

Digital Library

[8]

T. Ellman. Generalizing logic circuit designs by analyzing proofs of correctness. In IJCAI, volume 1, pages 643--646, 1985.

Digital Library

[9]

T. Ellman. Explanation-based learning: a survey of programs and perspectives. ACM Computing Surveys, 21(2):163--221, June 1989.

Digital Library

[10]

M. Gandhe and G. Venkatesh. Improving prolog performance by inductive proof generalizations. In Knowledge Based Computer Systems, 1990.

Digital Library

[11]

S.Z. Guyer and C. Lin. Broadway: A compiler for exploiting the domain-specific semantics of software libraries. Proceedings of IEEE, 93(2), 2005.

[12]

C. Haack and J.B. Wells. Type error slicing in implicitly typed higher-order languages. Science of Computer Programming, 50(1-3):189--224, 2004.

Digital Library

[13]

R. Joshi, G. Nelson, and K. Randall. Denali: a goal-directed superoptimizer. In PLDI, June 2002.

Digital Library

[14]

S. Kundu, Z. Tatlock, and S. Lerner. Proving optimizations correct using parameterized program equivalence. In PLDI, 2009.

Digital Library

[15]

S. Lerner, T. Millstein, E. Rice, and C. Chambers. Automated soundness proofs for dataflow analyses and transformations via local rules. In POPL, 2005.

Digital Library

[16]

H. Massalin. Superoptimizer: a look at the smallest program. In ASPLOS, 1987.

[17]

A. McGovern, J.E.B. Moss, and A.G. Barto. Building a basic block instruction scheduler with reinforcement learning and rollouts. Machine Learning, Special Issue on Reinforcement Learning, 49(2/3):141--160, May 2002.

Digital Library

[18]

R. Millner. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 1978.

[19]

M. Stephenson and S. Amarasinghe. Predicting unroll factors using supervised classification. In CGO, Mar. 2005.

Digital Library

[20]

M. Stephenson, S. Amarasinghe, M. Martin, and U.-M. O'Reilly. Meta optimization: Improving compiler heuristics with machine learning. In PLDI, June 2003.

Digital Library

[21]

R. Tate, M. Stepp, and S. Lerner. Generating compiler optimizations from proofs. Technical report, University of California, San Diego, Nov. 2009.

[22]

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

Digital Library

[23]

S.W.K. Tjiang and J.L. Hennessy. Sharlit -- A tool for building optimizers. In PLDI, 1992.

Digital Library

[24]

D.L. Whitfield and M.L. Soffa. An approach for exploring code improving transformations. ACM Transactions on Programming Languages and Systems, 19(6):1053--1084, Nov. 1997.

Digital Library

Cited By

Mukherjee MRegehr J(2024)Hydra: Generalizing Peephole Optimizations with Program SynthesisProceedings of the ACM on Programming Languages10.1145/36498378:OOPSLA1(725-753)Online publication date: 29-Apr-2024
https://dl.acm.org/doi/10.1145/3649837
Premtoon VKoppel JSolar-Lezama ADonaldson ATorlak E(2020)Semantic code search via equational reasoningProceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/3385412.3386001(1066-1082)Online publication date: 11-Jun-2020
https://dl.acm.org/doi/10.1145/3385412.3386001
Doerfert JHomerding BFinkel H(2019)Performance Exploration Through Optimistic Static Program AnnotationsHigh Performance Computing10.1007/978-3-030-20656-7_13(247-268)Online publication date: 17-May-2019
https://doi.org/10.1007/978-3-030-20656-7_13
Show More Cited By

Index Terms

Generating compiler optimizations from proofs
1. Software and its engineering
  1. Software notations and tools
    1. Compilers

Recommendations

Generating compiler optimizations from proofs
POPL '10

We present an automated technique for generating compiler optimizations from examples of concrete programs before and after improvements have been made to them. The key technical insight of our technique is that a proof of equivalence between the ...
The Intel labs Haskell research compiler
Haskell '13

The Glasgow Haskell Compiler (GHC) is a well supported optimizing compiler for the Haskell programming language, along with its own extensions to the language and libraries. Haskell's lazy semantics imposes a runtime model which is in general difficult ...
The Intel labs Haskell research compiler
Haskell '13: Proceedings of the 2013 ACM SIGPLAN symposium on Haskell

The Glasgow Haskell Compiler (GHC) is a well supported optimizing compiler for the Haskell programming language, along with its own extensions to the language and libraries. Haskell's lazy semantics imposes a runtime model which is in general difficult ...

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences

POPL '10: Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

January 2010

520 pages

ISBN:9781605584799

DOI:10.1145/1706299

General Chair:
Manuel Hermenegildo
IMDEA-Software and T.U. of Madrid, Spain
,
Program Chair:
Jens Palsberg
UCLA, University of California, Los Angeles

ACM SIGPLAN Notices Volume 45, Issue 1
POPL '10
January 2010
500 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/1707801
Issue’s Table of Contents

Copyright © 2010 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]

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

In-Cooperation

SIGACT: ACM Special Interest Group on Algorithms and Computation Theory

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 17 January 2010

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

POPL '10

Sponsor:

SIGPLAN

POPL '10: The 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

January 17 - 23, 2010

Madrid, Spain

Acceptance Rates

Overall Acceptance Rate 824 of 4,130 submissions, 20%

Upcoming Conference

POPL '25

Sponsor:
sigplan

The 52nd Annual ACM SIGPLAN Symposium on Principles of Programming Languages

January 19 - 25, 2025

Denver , CO , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

24
Total Citations
View Citations
653
Total Downloads

Downloads (Last 12 months)34
Downloads (Last 6 weeks)9

Reflects downloads up to 23 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Mukherjee MRegehr J(2024)Hydra: Generalizing Peephole Optimizations with Program SynthesisProceedings of the ACM on Programming Languages10.1145/36498378:OOPSLA1(725-753)Online publication date: 29-Apr-2024
https://dl.acm.org/doi/10.1145/3649837
Premtoon VKoppel JSolar-Lezama ADonaldson ATorlak E(2020)Semantic code search via equational reasoningProceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/3385412.3386001(1066-1082)Online publication date: 11-Jun-2020
https://dl.acm.org/doi/10.1145/3385412.3386001
Doerfert JHomerding BFinkel H(2019)Performance Exploration Through Optimistic Static Program AnnotationsHigh Performance Computing10.1007/978-3-030-20656-7_13(247-268)Online publication date: 17-May-2019
https://doi.org/10.1007/978-3-030-20656-7_13
Ginsbach PCrawford LO'Boyle MDubach CXue J(2018)CAnDL: a domain specific language for compiler analysisProceedings of the 27th International Conference on Compiler Construction10.1145/3178372.3179515(151-162)Online publication date: 24-Feb-2018
https://dl.acm.org/doi/10.1145/3178372.3179515
Gupta SSaxena AMahajan ABansal S(2018)Effective Use of SMT Solvers for Program Equivalence Checking Through Invariant-Sketching and Query-DecompositionTheory and Applications of Satisfiability Testing – SAT 201810.1007/978-3-319-94144-8_22(365-382)Online publication date: 26-Jun-2018
https://doi.org/10.1007/978-3-319-94144-8_22
Dotzler GKamp MKreutzer PPhilippsen MBodden ESchäfer WDeursen AZisman A(2017)More accurate recommendations for method-level changesProceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering10.1145/3106237.3106276(798-808)Online publication date: 21-Aug-2017
https://dl.acm.org/doi/10.1145/3106237.3106276
Dahiya MBansal S(2017)Black-Box Equivalence Checking Across Compiler OptimizationsProgramming Languages and Systems10.1007/978-3-319-71237-6_7(127-147)Online publication date: 19-Nov-2017
https://doi.org/10.1007/978-3-319-71237-6_7
Lopes NMenendez DNagarakatte SRegehr J(2015)Provably correct peephole optimizations with aliveACM SIGPLAN Notices10.1145/2813885.273796550:6(22-32)Online publication date: 3-Jun-2015
https://dl.acm.org/doi/10.1145/2813885.2737965
Lopes NMenendez DNagarakatte SRegehr JGrove DBlackburn S(2015)Provably correct peephole optimizations with aliveProceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/2737924.2737965(22-32)Online publication date: 3-Jun-2015
https://dl.acm.org/doi/10.1145/2737924.2737965
Lopes NMonteiro J(2014)Weakest Precondition Synthesis for Compiler OptimizationsProceedings of the 15th International Conference on Verification, Model Checking, and Abstract Interpretation - Volume 831810.1007/978-3-642-54013-4_12(203-221)Online publication date: 19-Jan-2014
https://dl.acm.org/doi/10.1007/978-3-642-54013-4_12
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 Table of Contents