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

Article

Proving correctness of compiler optimizations by temporal logic

Authors:

Carl Christian FrederiksenAuthors Info & Claims

POPL '02: Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Pages 283 - 294

https://doi.org/10.1145/503272.503299

Published: 01 January 2002 Publication History

Abstract

Many classical compiler optimizations can be elegantly expressed using rewrite rules of form: I ⇒ I′ if φ, where I, I′ are intermediate language instructions and φ is a property expressed in a temporal logic suitable for describing program data flow. Its reading: If the current program π contains an instruction of form I at some control point p, and if flow condition φ is satisfied at p, then replace I by I′.The purpose of this paper is to show how such transformations may be proven correct. Our methodology is illustrated by three familiar optimizations, dead code elimination, constant folding and code motion. The meaning of correctness is that for any program π, if Rewrite(π, π′, p,I ⇒ I′ if φ) then [[π]] = [[π′]], i.e. π and π′ have exactly the same semantics.

References

[1]

S. Abramsky and C. Hankin. Abstract Interpretation of Declarative Languages. Ellis-Horwood, 1987.]]

Digital Library

[2]

A.V. Aho and R. Sethi and J.D. Ullman. Compilers: Principles, Techniques, and Tools. Addison Wesley, 1986.]]

Digital Library

[3]

E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems (TOPLAS), 8(2):244-263, 1986.]]

Digital Library

[4]

R. Cleaveland and D. Jackson. Proceedings of First ACM SIGPLAN Workshop on Automated Analysis of Software. Paris, France, January 1997.]]

[5]

P. Cousot and R. Cousot, Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fix-points. In Fourth ACM Symposium on Principles of Programming Languages, Los Angeles, California, January 1977, pp. 238-252, New York: ACM, 1977.]]

Digital Library

[6]

P. Cousot, Semantic foundations of program analysis, in S.S. Muchnick and N.D. Jones (eds.), Program Flow Analysis: Theory and Applications, chapter 10, pp. 303-342, Englewood Cliffs, NJ: Prentice Hall, 1981.]]

[7]

C.C. Frederiksen. Correctness of classical compiler optimizations using CTL. Unpublished TOPPS report, University of Copenhagen, 2001. http://www.diku.dk/research-groups/ topps/bibliography/2001.html#D-443]]

[8]

Th. Hafer and W. Thomas. Computation tree logic CTL and path quantifiers in the monadic theory of the binary tree. In Automata, Languages and Programming Proceedings, ICALP'87, volume 267 of Lecture Notes in Computer Science, pages 267-279. Springer-Verlag, 1987.]]

Digital Library

[9]

K. Havelund. Stepwise Development of a Denotational Stack Semantics. M.Sc. thesis, University of Copenhagen, 1984.]]

[10]

M. Hecht. Flow analysis of computer programs. North-Holland, 1977.]]

Digital Library

[11]

N.D. Jones (ed.), Semantics-Directed Compiler Generation. volume 94 of Lecture Notes in Computer Science, Springer-Verlag, 1980.]]

Digital Library

[12]

N.D. Jones. Semantique: Semantic-Based Program Manipulation Techniques. In Bulletin European Association for Theoretical Computer Science 39:74-83, 1989.]]

[13]

N.D. Jones and F. Nielson. Abstract Interpretation: a Semantics-Based Tool for Program Analysis. In Handbook of Logic in Computer Science, edited by S. Abramsky, D, Gabbay, T. Maibaum, pages 527-629, Oxford University Press, 1994.]]

Digital Library

[14]

J. Knoop and O. R. uthing and B. Steffen. Optimal Code Motion: Theory and Practice. ACM Transactions on Programming Languages and Systems (TOPLAS), 16(4):1117-1155, 1994.]]

Digital Library

[15]

D. Kozen, Efficient code certification. Technical Report 98-1661, Computer Science Department, Cornell University, January, 1998.]]

Digital Library

[16]

D. Kozen and M. Patron. Certification of compiler optimizations using Kleene algebra with tests. In J. Lloyd, V. Dahl, U. Furbach, M. Kerber, K.-K. Lau, C. Palamidessi, L. M. Pereira, Y. Sagiv, and P. J. Stuckey, eds, Proceedings of the 1st International Conference on Computational Logic (CL2000), Lecture Notes in Artificial Intelligence volume 1861, Springer-Verlag, London, July 2000, pp. 568-582.]]

Digital Library

[17]

O. Kupferman and A. Pnueli. Once and for all. In Proc. 10th IEEE Symposium on Logic in Computer Science, pages 25-35, San Diego, June 1995.]]

Digital Library

[18]

D. Lacey and O. de Moor. Imperative program transformation by rewriting. In Proc. 10th International Conf. on Compiler Construction, volume 1113 of Lecture Notes in Computer Science, pages 52-68. Springer-Verlag, 2001.]]

Digital Library

[19]

R. Milne and C. Strachey A Theory of Programming Language Semantics. Chapman and Hall, 1976.]]

Digital Library

[20]

S.S. Muchnick. Advanced Compiler Design and Implementation. Morgan Kaufmann, 1997.]]

Digital Library

[21]

S.S. Muchnick and N.D. Jones (eds.) Program Flow Analysis: Theory and Applications. Englewood Cliffs, NJ: Prentice Hall, 1981.]]

Digital Library

[22]

G. Necula, Proof-carrying code. In 24th ACM Symposium on Principles of Programming Languages, Paris, France, January 1997, pp. 106-119, New York: ACM, 1997.]]

Digital Library

[23]

F. Nielson. A Denotational Framework for Data Flow Analysis. Acta Informatica, 18:265-287, 1982.]]

Digital Library

[24]

F. Nielson. Semantic Foundations of Data Flow Analysis. M.Sc. thesis, Aarhus University, DAIMI PB-131, 1981.]]

[25]

F. Nielson, H.R. Nielson and C. Hankin. Principles of Program Analysis. Springer-Verlag, 1999.]]

Digital Library

[26]

S. S. Pinter and P. Wolper. A temporal logic for reasoning about partially ordered computations. In Proc. 3rd ACM Symposium on Principles of Distributed Computing, pages 28-37, 1984.]]

Digital Library

[27]

A. Podelski, B. Steffen, M. Vardi. Schloss Ringberg Seminar: Model Checking and Program Analysis. Workshop, February 2000, Bavaria.]]

[28]

T. Rus and E. Van Wyk. Using model checking in a parallelizing compiler. Parallel Processing Letters, 8(4):459-471, 1998.]]

[29]

D.A. Schmidt. Data- ow analysis is model checking of abstract interpretations. In Proc. of 25th ACM Symposium on Principles of Programming Languages, ACM, 1998.]]

Digital Library

[30]

D.A. Schmidt, B. Steffen. Program analysis as model checking of abstract interpretations. In Proc. of 5th Static Analysis Symposium, G. Levi. ed., Pisa, volume 1503 of Lecture Notes in Computer Science, Springer-Verlag, 1998.]]

[31]

Paul A. Steckler and Mitchell Wand. Lightweight Closure Conversion. ACM Transactions on Programming Languages and Systems, ACM, 19(1):48-86, January 1997.]]

Digital Library

[32]

B. Steffen, A. Claen, M. Klein, J. Knoop, T. Margaria. The Fixpoint Analysis Machine. In Proc. of the 6th International Conference on Concurrency Theory (CONCUR'95), J. Lee, S. Smolka eds., Philadelphia, Pennsylvania (USA), volume 962 of Lecture Notes in Computer Science, Springer-Verlag, pp. 72-87, 1995.]]

Digital Library

[33]

G. Winskel. The Formal Semantics of Programming Languages. Boston, MA: the MIT Press, 1993.]]

Digital Library

[34]

P. Wolper. On the relation of programs and computations to models of temporal logic. In Proc. Temporal Logic in Specification, volume 398 of Lecture Notes in Computer Science, pages 75-123. Springer-Verlag, 1987.]]

Digital Library

Cited By

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
Doroshenko AYatsenko O(2021)Term Rewriting-Based ProgrammingFormal and Adaptive Methods for Automation of Parallel Programs Construction10.4018/978-1-5225-9384-3.ch003(76-111)Online publication date: 2021
https://doi.org/10.4018/978-1-5225-9384-3.ch003
D'Elia DDemetrescu C(2018)On-stack replacement, distilledACM SIGPLAN Notices10.1145/3296979.319239653:4(166-180)Online publication date: 11-Jun-2018
https://dl.acm.org/doi/10.1145/3296979.3192396
Show More Cited By

Proving correctness of compiler optimizations by temporal logic
1. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
  2. Software notations and tools
2. Theory of computation
  1. Semantics and reasoning
    1. Program reasoning

Recommendations

Proving correctness of compiler optimizations by temporal logic

Many classical compiler optimizations can be elegantly expressed using rewrite rules of form: I ⇒ I′ if φ, where I, I′ are intermediate language instructions and φ is a property expressed in a temporal logic suitable for describing program data flow. ...
Proving Correctness of a Compiler Using Step-indexed Logical Relations

In this paper we prove the correctness of a compiler for a call-by-name language using step-indexed logical relations and biorthogonality. The source language is an extension of the simply typed lambda-calculus with recursion, and the target language is ...
Constructive linear-time temporal logic: Proof systems and Kripke semantics

In this paper we study a version of constructive linear-time temporal logic (LTL) with the ''next'' temporal operator. The logic is originally due to Davies, who has shown that the proof system of the logic corresponds to a type system for binding-time ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

POPL '02: Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages

January 2002

351 pages

ISBN:1581134509

DOI:10.1145/503272

Conference Chair:
John Launchbury
OGI and Galois Connections
,
Program Chair:
John C. Mitchell
Stanford University

ACM SIGPLAN Notices Volume 37, Issue 1
Jan. 2002
342 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/565816
Issue’s Table of Contents

Copyright © 2002 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: 01 January 2002

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Conference

POPL02

Sponsor:

POPL02: The 29th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages 2002

January 16 - 18, 2002

Oregon, Portland

Acceptance Rates

POPL '02 Paper Acceptance Rate 28 of 128 submissions, 22%;

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

75
Total Citations
View Citations
756
Total Downloads

Downloads (Last 12 months)10
Downloads (Last 6 weeks)1

Reflects downloads up to 14 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

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
Doroshenko AYatsenko O(2021)Term Rewriting-Based ProgrammingFormal and Adaptive Methods for Automation of Parallel Programs Construction10.4018/978-1-5225-9384-3.ch003(76-111)Online publication date: 2021
https://doi.org/10.4018/978-1-5225-9384-3.ch003
D'Elia DDemetrescu C(2018)On-stack replacement, distilledACM SIGPLAN Notices10.1145/3296979.319239653:4(166-180)Online publication date: 11-Jun-2018
https://dl.acm.org/doi/10.1145/3296979.3192396
D'Elia DDemetrescu CFoster JGrossman D(2018)On-stack replacement, distilledProceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/3192366.3192396(166-180)Online publication date: 11-Jun-2018
https://dl.acm.org/doi/10.1145/3192366.3192396
Bissyandé TRéveillère LLawall JBromberg YMuller G(2015)Implementing an embedded compiler using program transformation rulesSoftware—Practice & Experience10.1002/spe.222545:2(177-196)Online publication date: 1-Feb-2015
https://dl.acm.org/doi/10.1002/spe.2225
Sorva JKaravirta VMalmi L(2013)A Review of Generic Program Visualization Systems for Introductory Programming EducationACM Transactions on Computing Education10.1145/249082213:4(1-64)Online publication date: 1-Nov-2013
https://dl.acm.org/doi/10.1145/2490822
Fantechi AGnesi SLapadula AMazzanti FPugliese RTiezzi F(2012)A logical verification methodology for service-oriented computingACM Transactions on Software Engineering and Methodology10.1145/2211616.221161921:3(1-46)Online publication date: 3-Jul-2012
https://dl.acm.org/doi/10.1145/2211616.2211619
Shonle MGriswold WLerner S(2012)A framework for the checking and refactoring of crosscutting conceptsACM Transactions on Software Engineering and Methodology10.1145/2211616.221161821:3(1-47)Online publication date: 3-Jul-2012
https://dl.acm.org/doi/10.1145/2211616.2211618
Cremonesi PGarzotto FTurrin R(2012)Investigating the Persuasion Potential of Recommender Systems from a Quality PerspectiveACM Transactions on Interactive Intelligent Systems10.1145/2209310.22093142:2(1-41)Online publication date: 1-Jun-2012
https://dl.acm.org/doi/10.1145/2209310.2209314
Kaptein MDe Ruyter BMarkopoulos PAarts E(2012)Adaptive Persuasive SystemsACM Transactions on Interactive Intelligent Systems10.1145/2209310.22093132:2(1-25)Online publication date: 1-Jun-2012
https://dl.acm.org/doi/10.1145/2209310.2209313
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