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

article

Free access

Proving the correctness of heuristically optimized code

Author:

Hanan SametAuthors Info & Claims

Communications of the ACM, Volume 21, Issue 7

Pages 570 - 582

https://doi.org/10.1145/359545.359569

Published: 01 July 1978 Publication History

Abstract

A system for proving that programs written in a high level language are correctly translated to a low level language is described. A primary use of the system is as a postoptimization step in code generation. The low level language programs need not be generated by a compiler and in fact could be hand coded. Examples of the usefulness of such a system are given. Some interesting results are the ability to handle programs that implement recursion by bypassing the start of the program, and the detection and pinpointing of a wide class of errors in the low level language programs. The examples demonstrate that optimization of the genre of this paper can result in substantially faster operation and the saving of memory in terms of program and stack sizes.

References

[1]

Aho, A., and Ullman, J.D. The Theory of Parsing, Translation, and Compiling, Vol. 2. Prentice-Hall, Englewood Cliffs, N.J., 1973, p. 938.

Digital Library

[2]

Allen, F.E. Control flow analysis. SIGPLAN Notices (ACM), 5, 7 (July 1970), 1-19, 239-307.

Digital Library

[3]

Bobrow, R.J., Burton, R.R., and Lewis, D. UCI LISP Manual. Inform. and Comptr. Sci. Tech. Rep. No. 21, U. of California at Irvine, Oct. 1972.

[4]

Boyer, R.S., and Moore, J.S. Proving theorems about LISP functions. J. ACM 22, 1 (Jan. 1975), 129-144.

Digital Library

[5]

Burstall, R.M., and Darlington, J. Some transformations for developing recursive programs. Proc. 1975 Int. Conf. on Reliable Software, April 1975, pp. 465-472.

Digital Library

[6]

Digital Equipment Corp. PDP-10 System Reference Manual. Digital Equipment Corporation, Maynard, Mass., 1969.

[7]

Deutsch, L.P. An interactive program verifier. Ph.D. Th., Dept. Comptr. Sci., U. of California at Berkeley, May 1973.

[8]

Floyd, R.W. Assigning meanings to programs. Proceedings of a Symposium in Applied Mathematics, Vol. 19, Mathematical Aspects of Science, J.T. Schwartz, Ed., Amer. Math. Soc., Providence, R.I. 1967, pp. 19-32.

[9]

Gerhart, S.L. Correctness preserving program transformations. Proc. Second ACM Symp. on Principles of Programming Languages, Jan. 1975, pp. 54-66.

Digital Library

[10]

Hollander, C.R. Decompilation of object programs. Ph.D. Th., Tech. Rep. No. 54, Digital Syst. Lab., Dept. of Electr. Eng., Stanford U., Stanford, Calif., 1973.

Digital Library

[11]

King, J.C. A program verifier. Ph.D. Th., Dept. of Comptr. Sci., Carnegie-Mellon U., Pittsburgh, Pa., 1969.

Digital Library

[12]

King, J.C. Symbolic execution and program testing. Comm. A CM 19, 7 (July 1976), 385-394.

Digital Library

[13]

Knuth, D. Structured programming with GO TO statements. Rep. STAN-CS-74-416, Comptr. Sci. Dept., Stanford U., Stanford, Calif., May 1974.

[14]

Lee, J.A.N. Computer Semantics. Van Nostrand Reinhold, New York, 1972, 346-347. .

[15]

London, R.L. Correctness of two compilers for a LISP subset. Stanford Artif. Intell. Proj. Memo AIM-151, Comptr. Sci. Dept., Stanford U., Stanford, Calif., Oct. 1971.

Digital Library

[16]

London, R.L. The current state of proving programs correct. Proc. ACM 25th Annual Conf., 1972, pp. 39-46.

Digital Library

[17]

Loveman, D.B. Program improvement by source to source transformation. Proc. Third ACM Symp. on Principles of Programming Languages, Jan. 1976, p. 145.

Digital Library

[18]

McCarthy, J. Recursive functions of symbolic expressions and their computation by machine. Comm. ACM 3, 4 (April 1960), 184-195.

Digital Library

[19]

McCarthy, J. A basis for a mathematical theory of computation. In Computer Programming and Formal Systems, P. Braffort and D. Hirshberg, Eds, North Holland, Amsterdam, 1963.

[20]

Newell, A. Artificial intelligence and the concept of mind. In Computer Models of Thought and Language, R.C. Schank and K.M. Colby Eds., W.H. Freeman, San Francisco, 1973, pp. 1-60.

[21]

Quam, L.H., and Diffie, W. Stanford LISP 1.6 Manual. Stanford Artif. Intell. Proj. Operating Note 28.7, Comptr. Sci. Dept., Stanford U., Stanford, Calif., 1972.

[22]

Reiser, J.F., Ed. SAIL User Manual. Stanford Artif. Intell. Proj. Memo AIM-289, Comptr. Sci. Dept., Stanford U., Stanford, Calif., Aug. 1976.

[23]

Samet, H. Automatically proving the correctness of translations involving optimized code. Ph.D. Th., Stanford Artif. Intell. Proj. Memo AIM-259, Comptr. Sci. Dept., Stanford U., Stanford, Calif., 1975.

Digital Library

[24]

Samet, H. A study in automatic debugging of compilers. TR-545, Comptr. Sci. Dept., U. of Maryland, College Park, Md., 1977.

[25]

Samet, H. Equivalence and inequivalence of instances of formulas. TR-553, Comptr. Sci. Dept., U. of Maryland, College Park, Md., 1977.

[26]

Smith, D.C. MLISP. Stanford Artif. Intell. Proj. Memo AIM-135, Comptr. Sci. Dept., Stanford U., Stanford, Calif., Oct. 1970.

Digital Library

[27]

Suzuki, N. Verifying programs by algebraic and logical reductions. Proc. 1975 Int. Conf. on Reliable Software, April 1975, pp. 473-481.

Digital Library

[28]

Wegbreit, B. Property extraction in well-founded property sets. IEEE Tran. Software Eng. SE-I,31 (Sept. 1975), pp. 270-285.

Digital Library

[29]

Wegbreit, B. Goal-directed program transformation. Proc. Third ACM Symp. on Principles of Programming Languages, Jan. 1976, pp. 153-170.

Digital Library

Cited By

Laufer BGilbert TNissenbaum H(2023)Optimization’s Neglected Normative CommitmentsProceedings of the 2023 ACM Conference on Fairness, Accountability, and Transparency10.1145/3593013.3593976(50-63)Online publication date: 12-Jun-2023
https://dl.acm.org/doi/10.1145/3593013.3593976
Lim JNagarakatte SKandemir MJimborean AMoseley T(2019)Automatic equivalence checking for assembly implementations of cryptography librariesProceedings of the 2019 IEEE/ACM International Symposium on Code Generation and Optimization10.5555/3314872.3314880(37-49)Online publication date: 16-Feb-2019
https://dl.acm.org/doi/10.5555/3314872.3314880
Lim JNagarakatte S(2019)Automatic Equivalence Checking for Assembly Implementations of Cryptography Libraries2019 IEEE/ACM International Symposium on Code Generation and Optimization (CGO)10.1109/CGO.2019.8661180(37-49)Online publication date: Feb-2019
https://doi.org/10.1109/CGO.2019.8661180
Show More Cited By

Index Terms

Recommendations

A Machine Description Facility for Compiler Testing

Requirements for a machine description facility for compiler testing are discussed. The compiler testing procedure consists of proving that programs are correctly translated by the compiler at hand. This is achieved by use of a common intermediate ...
Compiler testing via symbolic interpretation
ACM '76: Proceedings of the 1976 annual conference

A method for compiler testing using symbolic interpretation is presented. This method is a cross between program proving and program testing. It is useful in demonstrating that programs are correctly translated from a high level language to a low level ...
Code Optimization Considerations in List Processing Systems

Code optimization is characterized as a time versus space tradeoff. Space optimizations are further decomposed into static and dynamic categories. Using this characterization, the optimization requirements of a list processing language such as LISP are ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Communications of the ACM

Communications of the ACM Volume 21, Issue 7

July 1978

86 pages

ISSN:0001-0782

EISSN:1557-7317

DOI:10.1145/359545

Editor:
Robert L. Ashenhurst
The Univ. of Chicago, Chicago, IL

Issue’s Table of Contents

Copyright © 1978 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: 01 July 1978

Published in CACM Volume 21, Issue 7

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

31
Total Citations
View Citations
404
Total Downloads

Downloads (Last 12 months)82
Downloads (Last 6 weeks)7

Reflects downloads up to 01 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Laufer BGilbert TNissenbaum H(2023)Optimization’s Neglected Normative CommitmentsProceedings of the 2023 ACM Conference on Fairness, Accountability, and Transparency10.1145/3593013.3593976(50-63)Online publication date: 12-Jun-2023
https://dl.acm.org/doi/10.1145/3593013.3593976
Lim JNagarakatte SKandemir MJimborean AMoseley T(2019)Automatic equivalence checking for assembly implementations of cryptography librariesProceedings of the 2019 IEEE/ACM International Symposium on Code Generation and Optimization10.5555/3314872.3314880(37-49)Online publication date: 16-Feb-2019
https://dl.acm.org/doi/10.5555/3314872.3314880
Lim JNagarakatte S(2019)Automatic Equivalence Checking for Assembly Implementations of Cryptography Libraries2019 IEEE/ACM International Symposium on Code Generation and Optimization (CGO)10.1109/CGO.2019.8661180(37-49)Online publication date: Feb-2019
https://doi.org/10.1109/CGO.2019.8661180
Kang JKim YSong YLee JPark SShin MKim YCho SChoi JHur CYi K(2018)Crellvm: verified credible compilation for LLVMACM SIGPLAN Notices10.1145/3296979.319237753:4(631-645)Online publication date: 11-Jun-2018
https://dl.acm.org/doi/10.1145/3296979.3192377
Kang JKim YSong YLee JPark SShin MKim YCho SChoi JHur CYi KFoster JGrossman D(2018)Crellvm: verified credible compilation for LLVMProceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/3192366.3192377(631-645)Online publication date: 11-Jun-2018
https://dl.acm.org/doi/10.1145/3192366.3192377
Mullen EPernsteiner SWilcox JTatlock ZGrossman D(2018)Œuf: minimizing the Coq extraction TCBProceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs - CPP 201810.1145/3176245.3167089(172-185)Online publication date: 2018
https://doi.org/10.1145/3176245.3167089
Mullen EPernsteiner SWilcox JTatlock ZGrossman DAndronick JFelty A(2018)Œuf: minimizing the Coq extraction TCBProceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3167089(172-185)Online publication date: 8-Jan-2018
https://dl.acm.org/doi/10.1145/3167089
Lopes NMenendez DNagarakatte SRegehr J(2018)Practical verification of peephole optimizations with AliveCommunications of the ACM10.1145/316606461:2(84-91)Online publication date: 23-Jan-2018
https://dl.acm.org/doi/10.1145/3166064
Lim JGanapathy VNagarakatte SBielova NGaboardi M(2017)Compiler Optimizations with Retrofitting TransformationsProceedings of the 2017 Workshop on Programming Languages and Analysis for Security10.1145/3139337.3139343(37-42)Online publication date: 30-Oct-2017
https://dl.acm.org/doi/10.1145/3139337.3139343
Long YHu X(2017)Spatial Partition-Based Particle Filtering for Data Assimilation in Wildfire Spread SimulationACM Transactions on Spatial Algorithms and Systems10.1145/30994713:2(1-33)Online publication date: 24-Aug-2017
https://dl.acm.org/doi/10.1145/3099471
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

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