Semantic Transformation Framework for Rewriting Rules
Pages 1 - 13
Abstract
Semantics-preserving source-to-source program transformations, such as optimization and refactoring, are essential for software development. Such transformations are often defined by rewriting rules describing which part of a program must be replaced with which subprogram. The main obstacle to designing a transformation is to prove its semantics preservation. Rewriting-rule-based frameworks alleviate this difficulty by giving proof guidelines or automating the proofs. Unfortunately, each framework is applicable to a restricted set of transformations due to a fixed definition of semantics preservation. Cousot and Cousot’s semantic transformation framework resolves this problem by leaving a space for its users to define a proper semantics preservation property. However, the framework does not exploit the characteristic of rewriting rules and fails to ease the proofs. In this work, we define a semantic transformation framework tailored to rewriting rules by refining Cousot and Cousot’s framework. Our framework facilitates modular proofs by providing syntax-directed guidelines and theorems that simplify proofs. We show the versatility of our framework by proving the semantics preservation of six well-known transformations.
References
[1]
Uwe Aß mann. 2000. Graph rewrite systems for program optimization. ACM Transactions on Programming Languages and Systems (TOPLAS), 22, 4 (2000), 583–637. https://doi.org/10.1145/363911.363914
[2]
Gilles Barthe, Benjamin Grégoire, César Kunz, and Tamara Rezk. 2006. Certificate Translation for Optimizing Compilers. In Proceedings of the 13th International Symposium on Static Analysis, SAS 2006. Springer, 301–317. https://doi.org/10.1007/11823230_20
[3]
Nick Benton. 2004. Simple relational correctness proofs for static analyses and program transformations. In Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2004. ACM, 14–25. https://doi.org/10.1145/964001.964003
[4]
Yves Bertot, Benjamin Grégoire, and Xavier Leroy. 2004. A Structured Approach to Proving Compiler Optimizations Based on Dataflow Analysis. In Types for Proofs and Programs, International Workshop, TYPES 2004. Springer, 66–81. https://doi.org/10.1007/11617990_5
[5]
Patrick Cousot. 2021. Principles of Abstract Interpretation. MIT Press.
[6]
Patrick Cousot and Radhia Cousot. 2002. Systematic design of program transformation frameworks by abstract interpretation. In Proceedings of the 29th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2002. ACM, 178–190. https://doi.org/10.1145/503272.503290
[7]
Carl Christian Frederiksen. 2002. Correctness of Classical Compiler Optimizations using CTL. Electronic Notes in Theoretical Computer Science, 65, 2 (2002), 37–51. issn:1571-0661 https://doi.org/10.1016/S1571-0661(04)80395-5
[8]
Clément Hurlin. 2009. Automatic Parallelization and Optimization of Programs by Proof Rewriting. In Proceedings of the 16th International Symposium on Static Analysis, SAS 2009. Springer, 52–68. https://doi.org/10.1007/978-3-642-03237-0_6
[9]
Dexter Kozen. 1997. Kleene Algebra with Tests. ACM Transactions on Programming Languages and Systems (TOPLAS), 19, 3 (1997), 427–443. https://doi.org/10.1145/256167.256195
[10]
Dexter Kozen and Maria-Christina Patron. 2000. Certification of Compiler Optimizations Using Kleene Algebra with Tests. In Proceedings of the First International Conference on Computational Logic, CL 2000. Springer, 568–582. https://doi.org/10.1007/3-540-44957-4_38
[11]
Sudipta Kundu, Zachary Tatlock, and Sorin Lerner. 2009. Proving optimizations correct using parameterized program equivalence. In Proceedings of the 2009 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2009. ACM, 327–337. https://doi.org/10.1145/1542476.1542513
[12]
David Lacey and Oege de Moor. 2001. Imperative Program Transformation by Rewriting. In Proceedings of the 10th International Conference on Compiler Construction, CC 2001. Springer, 52–68. https://doi.org/10.1007/3-540-45306-7_5
[13]
David Lacey, Neil D. Jones, Eric Van Wyk, and Carl Christian Frederiksen. 2002. Proving correctness of compiler optimizations by temporal logic. In Proceedings of the 29th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2002. ACM, 283–294. https://doi.org/10.1145/503272.503299
[14]
David Lacey, Neil D. Jones, Eric Van Wyk, and Carl Christian Frederiksen. 2004. Compiler Optimization Correctness by Temporal Logic. Higher-Order and Symbolic Computation, 17, 3 (2004), 173–206. https://doi.org/10.1023/B:LISP.0000029444.99264.c0
[15]
Sorin Lerner, Todd D. Millstein, and Craig Chambers. 2003. Automatically proving the correctness of compiler optimizations. In Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation, PLDI 2003, Ron Cytron and Rajiv Gupta (Eds.). ACM, 220–231. https://doi.org/10.1145/781131.781156
[16]
Xavier Leroy. 2006. Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2006. ACM, 42–54. https://doi.org/10.1145/1111037.1111042
[17]
John M. Li and Andrew W. Appel. 2021. Deriving efficient program transformations from rewrite rules. Proc. ACM Program. Lang., 5, ICFP (2021), 1–29. https://doi.org/10.1145/3473579
[18]
Peter Lipps, Ulrich Möncke, and Reinhard Wilhelm. 1988. OPTRAN - A Language/System for the Specification of Program Transformations: System Overview and Experiences. In Proceedings of the 2nd CCHSC Workshop on Compiler Compilers and High Speed Compilation. Springer, 52–65. https://doi.org/10.1007/3-540-51364-7_4
[19]
Nuno P. Lopes, David Menendez, Santosh Nagarakatte, and John Regehr. 2015. Provably correct peephole optimizations with alive. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2015. ACM, 22–32. https://doi.org/10.1145/2737924.2737965
[20]
William Mansky and Elsa L. Gunter. 2010. A Framework for Formal Verification of Compiler Optimizations. In Proceedings of the First International Conference on Interactive Theorem Proving, ITP 2010, Matt Kaufmann and Lawrence C. Paulson (Eds.). Springer, 371–386. https://doi.org/10.1007/978-3-642-14052-5_26
[21]
Simon Peyton Jones, Andrew Tolmach, and Tony Hoare. 2001. Playing by the rules: rewriting as a practical optimisation technique in GHC. In Haskell Workshop 2001.
[22]
Ando Saabas and Tarmo Uustalu. 2008. Program and proof optimizations with type systems. The Journal of Logic and Algebraic Programming, 77, 1-2 (2008), 131–154. https://doi.org/10.1016/j.jlap.2008.05.007
[23]
Zachary Tatlock and Sorin Lerner. 2010. Bringing extensibility to verified compilers. In Proceedings of the 2010 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2010. ACM, 111–121. https://doi.org/10.1145/1806596.1806611
[24]
Eelco Visser. 2001. A Survey of Rewriting Strategies in Program Transformation Systems. Electronic Notes in Theoretical Computer Science, 57 (2001), 109–143. issn:1571-0661 https://doi.org/10.1016/S1571-0661(04)00270-1
[25]
Deborah 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. https://doi.org/10.1145/267959.267960
Index Terms
- Semantic Transformation Framework for Rewriting Rules
Recommendations
Rule-based transformation of graph rewriting rules
Higher-order functions - the ones which manipulate other functions - have a fundamental role in Computer Science, specially in areas such as functional programming and theory of computation. Graph transformation - the rule-based modification of graphs - ...
On validation of ATL transformation rules by transformation models
MoDeVVa: Proceedings of the 8th International Workshop on Model-Driven Engineering, Verification and ValidationModel-to-model transformations constitute an important ingredient in model-driven engineering. As real world transformations are complex, systematic approaches are required to ensure their correctness. The ATLAS Transformation Language (ATL) is a mature ...
Program transformation by templates based on term rewriting
PPDP '05: Proceedings of the 7th ACM SIGPLAN international conference on Principles and practice of declarative programmingHuet and Lang (1978) presented a framework of automated program transformation based on lambda calculus in which programs are transformed according to a given program transformation template. They introduced a second-order matching algorithm of simply-...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Copyright © 2023 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
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 15 January 2023
Check for updates
Author Tags
Qualifiers
- Research-article
Funding Sources
- National Research Foundation of Korea
- Institute for Information and communications Technology Promotion
- Samsung Electronics Co., Ltd
Conference
POPL '23
Sponsor:
POPL '23: The 50th Annual ACM SIGPLAN Symposium on Principles of Programming Languages
January 16 - 17, 2023
MA, Boston, USA
Acceptance Rates
Overall Acceptance Rate 66 of 120 submissions, 55%
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 150Total Downloads
- Downloads (Last 12 months)57
- Downloads (Last 6 weeks)2
Reflects downloads up to 14 Dec 2024
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in