research-article

Open access

Deriving efficient program transformations from rewrite rules

Authors:

Andrew W. AppelAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 5, Issue ICFP

Article No.: 74, Pages 1 - 29

https://doi.org/10.1145/3473579

Published: 19 August 2021 Publication History

Abstract

An efficient optimizing compiler can perform many cascading rewrites in a single pass, using auxiliary data structures such as variable binding maps, delayed substitutions, and occurrence counts. Such optimizers often perform transformations according to relatively simple rewrite rules, but the subtle interactions between the data structures needed for efficiency make them tricky to write and trickier to prove correct. We present a system for semi-automatically deriving both an efficient program transformation and its correctness proof from a list of rewrite rules and specifications of the auxiliary data structures it requires. Dependent types ensure that the holes left behind by our system (for the user to fill in) are filled in correctly, allowing the user low-level control over the implementation without having to worry about getting it wrong. We implemented our system in Coq (though it could be implemented in other logics as well), and used it to write optimization passes that perform uncurrying, inlining, dead code elimination, and static evaluation of case expressions and record projections. The generated implementations are sometimes faster, and at most 40% slower, than hand-written counterparts on a small set of benchmarks; in some cases, they require significantly less code to write and prove correct.

Supplementary Material

Auxiliary Presentation Video (icfp21main-p68-p-video.mp4)

This is a presentation video of my talk at ICFP 2021 on our paper accepted in the research track, titled "Deriving Efficient Program Transformations From Rewrite Rules."

Download
85.26 MB

MP4 File (3473579.mp4)

Presentation Videos

Download
24.29 MB

References

[1]

Abhishek Anand, Andrew W. Appel, Greg Morrisett, Zoe Paraskevopoulou, Randy Pollack, Olivier Savary Belanger, Matthieu Sozeau, and Matthew Weaver. 2017. CertiCoq: A verified compiler for Coq. In The Third International Workshop on Coq for Programming Languages (CoqPL).

[2]

Andrew W. Appel. 1994. Loop headers in λ -calculus or CPS. Lisp and Symbolic Computation, 7, 4 (1994), 337–343.

Digital Library

[3]

Andrew W. Appel and Trevor Jim. 1997. Shrinking lambda expressions in linear time. Journal of Functional Programming, 7, 5 (1997), 515–540.

Digital Library

[4]

Andrew W. Appel and David B. MacQueen. 1991. Standard ML of New Jersey. In 3rd International Symp. on Prog. Lang. Implementation and Logic Programming, Martin Wirsing (Ed.). Springer-Verlag, New York. 1–13.

[5]

Nick Benton, Andrew Kennedy, Sam Lindley, and Claudio Russo. 2004. Shrinking reductions in SML. NET. In Symposium on Implementation and Application of Functional Languages. 142–159.

[6]

Pierre Chambart, Mark Shinwell, Leo White, and Damien Doligez. 2016. Optimization with Flambda. https://caml.inria.fr/pub/docs/manual-ocaml/flambda.html

[7]

Ron Cytron, Jeanne Ferrante, Barry K. Rosen, Mark N. Wegman, and F. Kenneth Zadeck. 1991. Efficiently Computing Static Single Assignment Form and the Control Dependence Graph. ACM Transactions on Programming Languages and Systems, 13, 4 (1991), October, 451–490.

Digital Library

[8]

Martin Erwig and Simon Peyton Jones. 2001. Pattern guards and transformational patterns. Electronic Notes in Theoretical Computer Science, 41, 1 (2001), 3.

[9]

Gérard Huet. 1997. Functional pearl. J. functional programming, 7, 5 (1997), 549–554.

[10]

Andrew Kennedy. 2007. Compiling with Continuations, Continued. SIGPLAN Not., 42, 9 (2007), 177–190.

Digital Library

[11]

Eugene E Kohlbecker and Mitchell Wand. 1987. Macro-by-example: Deriving syntactic transformations from their specifications. In Proceedings of the 14th ACM SIGACT-SIGPLAN symposium on Principles of programming languages. 77–84.

Digital Library

[12]

D. Kranz, R. Kelsey, J. Rees, P. Hudak, J. Philbin, and N. Adams. 1986. ORBIT: An optimizing compiler for Scheme. SIGPLAN Notices (Proc. Sigplan ’86 Symp. on Compiler Construction), 21, 7 (1986), July, 219–33.

[13]

Ramana Kumar, Magnus O Myreen, Michael Norrish, and Scott Owens. 2014. CakeML: a verified implementation of ML. ACM SIGPLAN Notices, 49, 1 (2014), 179–191.

Digital Library

[14]

David Lacey and Oege De Moor. 2001. Imperative program transformation by rewriting. In International Conference on Compiler Construction. 52–68.

[15]

Sorin Lerner, Todd Millstein, and Craig Chambers. 2005. Cobalt: A language for writing provably-sound compiler optimizations. Electronic Notes in Theoretical Computer Science, 132, 1 (2005), 5–17.

Digital Library

[16]

Sorin Lerner, Todd Millstein, Erika Rice, and Craig Chambers. 2005. Automated Soundness Proofs for Dataflow Analyses and Transformations via Local Rules. SIGPLAN Not., 40, 1 (2005), Jan., 364–377. issn:0362-1340 https://doi.org/10.1145/1047659.1040335

Digital Library

[17]

Xavier Leroy. 2012. The CompCert verified compiler.

[18]

William Mansky. 2014. Specifying and verifying program transformations with PTRANS. Ph.D. Dissertation. University of Illinois at Urbana-Champaign.

[19]

Jacob Matthews and Robert Bruce Findler. 2007. Operational semantics for multi-language programs. ACM SIGPLAN Notices, 42, 1 (2007), 3–10.

Digital Library

[20]

Georg Neis, Chung-Kil Hur, Jan-Oliver Kaiser, Craig McLaughlin, Derek Dreyer, and Viktor Vafeiadis. 2015. Pilsner: a compositionally verified compiler for a higher-order imperative language. In Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming. 166–178.

Digital Library

[21]

Simon Peyton Jones and Simon Marlow. 2002. Secrets of the Glasgow Haskell Compiler Inliner. J. Funct. Program., 12, 5 (2002), July, 393–434. issn:0956-7968 https://doi.org/10.1017/S0956796802004331

Digital Library

[22]

Reudismam Rolim, Gustavo Soares, Loris D’Antoni, Oleksandr Polozov, Sumit Gulwani, Rohit Gheyi, Ryo Suzuki, and Björn Hartmann. 2017. Learning syntactic program transformations from examples. In 2017 IEEE/ACM 39th International Conference on Software Engineering (ICSE). 404–415.

Digital Library

[23]

Dipanwita Sarkar, Oscar Waddell, R Kent Dybvig, and EDUCATIONAL PEARL. 2005. A nanopass framework for compiler education. Journal of Functional Programming, 15, 5 (2005), 653.

Digital Library

[24]

Olivier Savary Bélanger and Andrew W. Appel. 2017. Shrink fast correctly!. In Proceedings of the 19th International Symposium on Principles and Practice of Declarative Programming. 49–60.

[25]

Matthieu Sozeau. 2010. Equations: A dependent pattern-matching compiler. In International Conference on Interactive Theorem Proving. 419–434.

Digital Library

[26]

Matthieu Sozeau, Abhishek Anand, Simon Boulier, Cyril Cohen, Yannick Forster, Fabian Kunze, Gregory Malecha, Nicolas Tabareau, and Théo Winterhalter. 2020. The MetaCoq Project. Journal of Automated Reasoning, 1–53.

[27]

Guy L. Steele. 1978. Rabbit: a compiler for Scheme. MIT, Cambridge, MA.

[28]

Gordon Stewart, Lennart Beringer, and Andrew W. Appel. 2012. Verified heap theorem prover by paramodulation. ACM SIGPLAN Notices, 47, 9 (2012), 3–14.

Digital Library

[29]

Ross Tate, Michael Stepp, and Sorin Lerner. 2010. Generating Compiler Optimizations from Proofs. SIGPLAN Not., 45, 1 (2010), Jan., 389–402. issn:0362-1340 https://doi.org/10.1145/1707801.1706345

Digital Library

[30]

Steven WK Tjiang and John L Hennessy. 1992. Sharlit—a tool for building optimizers. ACM SIGPLAN Notices, 27, 7 (1992), 82–93.

Digital Library

[31]

Eelco Visser. 2004. Program transformation with Stratego/XT. In Domain-specific program generation. Springer, 216–238.

[32]

Deborah L Whitfield and Mary Lou Soffa. 1997. An approach for exploring code improving transformations. ACM Transactions on Programming Languages and Systems (TOPLAS), 19, 6 (1997), 1053–1084.

Digital Library

[33]

Xuejun Yang, Yang Chen, Eric Eide, and John Regehr. 2011. Finding and understanding bugs in C compilers. ACM SIGPLAN Notices (PLDI’11), 46, 6 (2011), 283–294.

Cited By

Baziotis SKang DMendis C(2024)Dias: Dynamic Rewriting of Pandas CodeProceedings of the ACM on Management of Data10.1145/36393132:1(1-27)Online publication date: 26-Mar-2024
https://dl.acm.org/doi/10.1145/3639313
Balasubramanian AMajumdar RThinniyam RZetzsche G(2024)Reachability in Continuous Pushdown VASSProceedings of the ACM on Programming Languages10.1145/36332798:POPL(90-114)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3633279
Park JHong JRyu SBrady EPalsberg J(2023)Semantic Transformation Framework for Rewriting RulesProceedings of the 2023 ACM SIGPLAN International Workshop on Partial Evaluation and Program Manipulation10.1145/3571786.3573016(1-13)Online publication date: 15-Jan-2023
https://dl.acm.org/doi/10.1145/3571786.3573016
Show More Cited By

Index Terms

Deriving efficient program transformations from rewrite rules
1. Software and its engineering
  1. Software notations and tools
    1. Compilers
      1. Translator writing systems and compiler generators

Recommendations

Domain-specific languages and program generation with meta-AspectJ

Meta-AspectJ (MAJ) is a language for generating AspectJ programs using code templates. MAJ itself is an extension of Java, so users can interleave arbitrary Java code with AspectJ code templates. MAJ is a structured metaprogramming tool: a well-typed ...
Reusable, generic program analyses and transformations
GPCE '09

The optimizations in modern compilers are constructed for a predetermined set of primitive types. As a result, programmers are unable to exploit optimizations for user-defined types where these optimizations would be correct and beneficial. Moreover, ...
Automated soundness proofs for dataflow analyses and transformations via local rules
POPL '05: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages

We present Rhodium, a new language for writing compiler optimizations that can be automatically proved sound. Unlike our previous work on Cobalt, Rhodium expresses optimizations using explicit dataflow facts manipulated by local propagation and ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages

Proceedings of the ACM on Programming Languages Volume 5, Issue ICFP

August 2021

1011 pages

EISSN:2475-1421

DOI:10.1145/3482883

Issue’s Table of Contents

Copyright © 2021 Owner/Author.

This work is licensed under a Creative Commons Attribution International 4.0 License.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 19 August 2021

Published in PACMPL Volume 5, Issue ICFP

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Author Tags

Qualifiers

Research-article

Funding Sources

National Science Foundation

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

8
Total Citations
View Citations
524
Total Downloads

Downloads (Last 12 months)168
Downloads (Last 6 weeks)31

Reflects downloads up to 12 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Baziotis SKang DMendis C(2024)Dias: Dynamic Rewriting of Pandas CodeProceedings of the ACM on Management of Data10.1145/36393132:1(1-27)Online publication date: 26-Mar-2024
https://dl.acm.org/doi/10.1145/3639313
Balasubramanian AMajumdar RThinniyam RZetzsche G(2024)Reachability in Continuous Pushdown VASSProceedings of the ACM on Programming Languages10.1145/36332798:POPL(90-114)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3633279
Park JHong JRyu SBrady EPalsberg J(2023)Semantic Transformation Framework for Rewriting RulesProceedings of the 2023 ACM SIGPLAN International Workshop on Partial Evaluation and Program Manipulation10.1145/3571786.3573016(1-13)Online publication date: 15-Jan-2023
https://dl.acm.org/doi/10.1145/3571786.3573016
Li YSi Salem TNeglia GIoannidis S(2022)Online Caching Networks with Adversarial GuaranteesACM SIGMETRICS Performance Evaluation Review10.1145/3547353.352263250:1(91-92)Online publication date: 7-Jul-2022
https://dl.acm.org/doi/10.1145/3547353.3522632
Li TYang RQu GShi GYu CWierman ALow S(2022)Robustness and Consistency in Linear Quadratic Control with Untrusted PredictionsProceedings of the ACM on Measurement and Analysis of Computing Systems10.1145/35080386:1(1-35)Online publication date: 28-Feb-2022
https://dl.acm.org/doi/10.1145/3508038
Li YZhang QReps T(2022)Fast Graph Simplification for Interleaved-Dyck ReachabilityACM Transactions on Programming Languages and Systems10.1145/349242844:2(1-28)Online publication date: 27-May-2022
https://dl.acm.org/doi/10.1145/3492428
Jin HGuo BRoychoudhury RYao YKumar SAgarwal YHong J(2022)Exploring the Needs of Users for Supporting Privacy-Protective Behaviors in Smart HomesProceedings of the 2022 CHI Conference on Human Factors in Computing Systems10.1145/3491102.3517602(1-19)Online publication date: 29-Apr-2022
https://dl.acm.org/doi/10.1145/3491102.3517602
Li YSi Salem TNeglia GIoannidis SManjunath DNair JCarlsson NCohen ERobert P(2022)Online Caching Networks with Adversarial GuaranteesAbstract Proceedings of the 2022 ACM SIGMETRICS/IFIP PERFORMANCE Joint International Conference on Measurement and Modeling of Computer Systems10.1145/3489048.3522632(91-92)Online publication date: 6-Jun-2022
https://dl.acm.org/doi/10.1145/3489048.3522632

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Get Access

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 Article

Media

Figures

Other

Tables

View Issue’s Table of Contents