research-article

Proof optimization for partial redundancy elimination

Authors:

Tarmo UustaluAuthors Info & Claims

PEPM '08: Proceedings of the 2008 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation

Pages 91 - 101

https://doi.org/10.1145/1328408.1328422

Published: 07 January 2008 Publication History

Abstract

Partial redundancy elimination is a subtle optimization which performs common subexpression elimination and expression motion at the same time. In this paper, we use it as an example to promote and demonstrate the scalability of the technology of proof optimization. By this we mean automatic transformation of a given program's Hoare logic proof of functional correctness or resource usage into one of the optimized program, guided by a type-derivation representation of the result of the underlying dataflow analyses. A proof optimizer is a useful tool for the producer's side in a natural proof-carrying code scenario where programs are proved correct prior to optimizing compilation before transmission to the consumer.

We present a type-systematic description of the underlying analyses and of the optimization for the W<scp>hile</scp> language, demonstrate that the optimization is semantically sound and improving in a formulation using type-indexed relations, and then show that these arguments can be transferred to mechanical transformations of functional correctness/resource usage proofs in Hoare logics. For the improvement part, we instrument the standard semantics and Hoare logic so that evaluations of expressions become a resource.

References

[1]

D. Aspinall, L. Beringer, A. Momigliano. Optimisation validation. In Proc. 5th Int. Wksh. on Compiler Optimization Meets Compiler Verification, COCV '06 (Vienna, Apr. 2006), v. 176, n. 3 of Electron. Notes in Theor. Comput. Sci., pp. 37--59, 2007.

Digital Library

[2]

G. Barthe, B. Grégoire, C. Kunz, T. Rezk. Certificate translation for optimizing compilers. In K. Yi, ed., Proc. of 13th Int. Static Analysis Symp., SAS 2006 (Seoul, Aug. 2006), v. 4134 of Lect. Notes in Comput. Sci., pp. 301--317. Springer, 2006.

Digital Library

[3]

G. Barthe, T. Rezk, A. Saabas. Proof obligations preserving compilation. In T. Dimitrakos, F. Martinelli, P. Y. A. Ryan, S. Schneider, eds., Revised Selected Papers from 3rd Int. Wksh. on Formal Aspects in Security and Trust, FAST 2005 (Newcastle upon Tyne, July 2005), v. 3866 of Lect. Notes in Comput. Sci., pp. 112--126. Springer, 2006.

Digital Library

[4]

N. Benton. Simple relational correctness proofs for static analyses and program transformations. In Proc. of 31st ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, POPL 2004 (Venice, Jan. 2004), pp. 14--25, ACM Press, 2004.

Digital Library

[5]

D. Bronnikov. A practical adoption of partial redundancy elimination. ACM SIGPLAN Notices, v. 39, n. 8, pp. 49--53, 2004.

Digital Library

[6]

A. Chaieb. Proof-producing program analysis. In K. Barkaoui, A. Cavalcanti, A. Cerone, eds., Proc. of 3rd Int. Coll. on Theor. Aspects of Computing, ICTAC 2006 (Tunis, Nov. 2006), v. 4281 of Lect. Notes in Comput. Sci., pp. 287--301. Springer, 2006.

Digital Library

[7]

D. M. Dhamdhere. Practical adaptation of the global optimization algorithm of Morel and Renvoise. ACM Trans. on Program. Lang. and Syst., v. 13, n. 2, pp. 291--294, 1991.

Digital Library

[8]

D. M. Dhamdhere. E-path PRE-partial redundancy elimination made easy. ACM SIGPLAN Notices, v. 37, n. 8, pp. 53--65, 2002.

Digital Library

[9]

K. H. Drechsler, M. P. Stadel. A solution to a problem with Morel and Renvoise's ''Global optimization by suppression of partial redundancies''. ACM Trans. on Program. Lang. and Syst., v. 10, n. 4, pp. 635--640, 1988.

Digital Library

[10]

K. H. Drechsler, M. P. Stadel. A variation of Knoop, Rüthing and Steffen's ''Lazy code motion''. ACM SIGPLAN Notices, v. 28, n. 5, pp. 29--38, 1993.

Digital Library

[11]

M. J. Frade, A. Saabas, T. Uustalu. Foundational certification of dataflow analyses. In Proc. of 1st IEEE and IFIP Int. Symp on Theor. Aspects of Software Engineering, TASE 2007 (Shanghai, June 2007), pp. 107--116. IEEE CS Press, 2007.

Digital Library

[12]

J. Knoop, O. Rüthing, B. Steffen. Lazy code motion. In Proc. of PLDI '92 (San Francisco, CA, June 1992), pp. 224--234. ACM Press, 1992.

Digital Library

[13]

J. Knoop, O. Rüthing, B. Steffen. Optimal code motion: theory and practice. ACM Trans. on Program. Lang. and Syst., v. 16, n. 4, pp. 1117--1155, 1994.

Digital Library

[14]

S. Lerner, T. Millstein, C. Chambers. Automatically proving the correctness of compiler optimizations. In Proc. of PLDI '03 (San Diego, CA, June 2003), pp. 220--231. ACM Press, 2003.

Digital Library

[15]

S. Lerner, T. Millstein, E. Rice, C. Chambers. Automated soundness proofs for dataflow analyses and transformations via local rules. In Proc. of 32nd ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, POPL '05 (Long Beach, CA, Jan. 2005), pp. 364--377.

Digital Library

[16]

E. Morel, C. Renvoise. Global optimization by suppression of partial redundancies. Commun. of ACM, v. 22, n. 2, pp. 96--103, 1979.

Digital Library

[17]

H. R. Nielson, F. Nielson. Flow logic: a multi-paradigmatic approach to static analysis. In T. Æ. Mogensen, D. Smith, I. H. Sudborough, eds., The Essence of Computation, Complexity, Analysis, Transformation: Essays Dedicated to Neil D. Jones, v. 2566 of Lect. Notes in Comput. Sci., pp. 223--244. Springer, 2002.

Digital Library

[18]

V. K. Paleri, Y. N. Srikant, P. Shankar. Partial redundancy elimination: a simple, pragmatic, and provably correct algorithm. Sci. of Comput. Program., v. 48, n. 1, pp. 1--20, 2003.

Digital Library

[19]

A. Saabas, T. Uustalu. Program and proof optimizations with type systems. Submitted to J. of Logic and Algebraic Program.

[20]

A. Saabas, T. Uustalu. Type systems for optimizing stack-based code. In M. Huisman, F. Spoto, eds., Proc. of 2nd Wksh. on Bytecode Semantics, Verification, Analysis and Transformation, Bytecode 2007 (Braga, March 2007), v. 190, n. 1 of Electron. Notes in Theor. Comput. Sci., pp. 103--119. Elsevier, 2007.

Digital Library

[21]

S. Seo, H. Yang, K. Yi. Automatic construction of Hoare proofs from abstract interpretation results. In A. Ohori, ed., Proc. of 1st Asian Symp. on Programming Languages and Systems, APLAS 2003 (Beijing, Nov. 2003), v. 2895 of Lect. Notes in Comput. Sci., pp. 230--245. Springer, 2003.

[22]

J. Xue, J. Knoop. A fresh look at PRE as a maximum flow problem. In A. Mycroft, A. Zeller, eds., Proc. of 15th Int. Conf. on Compiler Construction, CC 2006 (Vienna, March 2006), Lect. Notes in Comput. Sci., v. 3923, pp. 139--154. Springer, 2006.

Digital Library

Cited By

Barthe GKunz C(2011)An Abstract Model of Certificate TranslationACM Transactions on Programming Languages and Systems (TOPLAS)10.1145/1985342.198534433:4(1-46)Online publication date: 1-Jul-2011
https://dl.acm.org/doi/10.1145/1985342.1985344
Beringer L(2010)Relational bytecode correlationsThe Journal of Logic and Algebraic Programming10.1016/j.jlap.2010.07.00579:7(483-514)Online publication date: Oct-2010
https://doi.org/10.1016/j.jlap.2010.07.005
Frade MSaabas AUustalu TPuebla GVidal G(2009)Bidirectional data-flow analyses, type-systematicallyProceedings of the 2009 ACM SIGPLAN workshop on Partial evaluation and program manipulation10.1145/1480945.1480965(141-150)Online publication date: 19-Jan-2009
https://dl.acm.org/doi/10.1145/1480945.1480965
Show More Cited By

Index Terms

Proof optimization for partial redundancy elimination
1. Software and its engineering
  1. Software notations and tools
    1. Compilers
2. Theory of computation
  1. Logic
    1. Programming logic
  2. Semantics and reasoning
    1. Program reasoning

Recommendations

Classical Logic with Partial Functions

We introduce a semantics for classical logic with partial functions, in which ill-typed formulas are guaranteed to have no truth value, so that they cannot be used in any form of reasoning. The semantics makes it possible to mix reasoning about types ...
Polymorphic lemmas and definitions in $\lambda$Prolog and Twelf

$\lambda$Prolog is known to be well-suited for expressing and implementing logics and inference systems. We show that lemmas and definitions in such logics can be implemented with a great economy of expression. We encode a higher-order logic using an ...
Cut-Elimination and Proof Schemata
Revised Selected Papers of the 10th International Tbilisi Symposium on Logic, Language, and Computation - Volume 8984

By Gentzen's famous Hauptsatz the cut-elimination theorem every proof in sequent calculus for first-order logic with cuts can be transformed into a cut-free proof; cut-free proofs are analytic and consist entirely of syntactic material of the end-...

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences

PEPM '08: Proceedings of the 2008 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation

January 2008

214 pages

ISBN:9781595939777

DOI:10.1145/1328408

General Chair:
John Hatcliff
Kansas State University, USA
,
Program Chairs:
Robert Glück
University of Copenhagen, Denmark
,
Oege de Moor
Oxford University, UK

Copyright © 2008 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: 07 January 2008

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

PEPM08

Sponsor:

PEPM08: Partial Evaluation and Program Manipulation

January 7 - 8, 2008

California, San Francisco, USA

Acceptance Rates

Overall Acceptance Rate 66 of 120 submissions, 55%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

4
Total Citations
View Citations
203
Total Downloads

Downloads (Last 12 months)2
Downloads (Last 6 weeks)0

Reflects downloads up to 20 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Barthe GKunz C(2011)An Abstract Model of Certificate TranslationACM Transactions on Programming Languages and Systems (TOPLAS)10.1145/1985342.198534433:4(1-46)Online publication date: 1-Jul-2011
https://dl.acm.org/doi/10.1145/1985342.1985344
Beringer L(2010)Relational bytecode correlationsThe Journal of Logic and Algebraic Programming10.1016/j.jlap.2010.07.00579:7(483-514)Online publication date: Oct-2010
https://doi.org/10.1016/j.jlap.2010.07.005
Frade MSaabas AUustalu TPuebla GVidal G(2009)Bidirectional data-flow analyses, type-systematicallyProceedings of the 2009 ACM SIGPLAN workshop on Partial evaluation and program manipulation10.1145/1480945.1480965(141-150)Online publication date: 19-Jan-2009
https://dl.acm.org/doi/10.1145/1480945.1480965
Barthe GGrégoire BPavlova M(2008)Preservation of Proof Obligations from Java to the Java Virtual MachineProceedings of the 4th international joint conference on Automated Reasoning10.1007/978-3-540-71070-7_7(83-99)Online publication date: 12-Aug-2008
https://dl.acm.org/doi/10.1007/978-3-540-71070-7_7

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