Article

Weakest Precondition Synthesis for Compiler Optimizations

Authors:

José MonteiroAuthors Info & Claims

VMCAI 2014: Proceedings of the 15th International Conference on Verification, Model Checking, and Abstract Interpretation - Volume 8318

Pages 203 - 221

https://doi.org/10.1007/978-3-642-54013-4_12

Published: 19 January 2014 Publication History

Abstract

Compiler optimizations play an increasingly important role in code generation. This is especially true with the advent of resourcelimited mobile devices. We rely on compiler optimizations to improve performance, reduce code size, and reduce power consumption of our programs.

Despite being a mature field, compiler optimizations are still designed and implemented by hand, and usually without providing any guarantee of correctness.

In addition to devising the code transformations, designers and implementers have to come up with an analysis that determines in which cases the optimization can be safely applied. In other words, the optimization designer has to specify a precondition that ensures that the optimization is semantics-preserving. However, devising preconditions for optimizations by hand is a non-trivial task. It is easy to specify a precondition that, although correct, is too restrictive, and therefore misses some optimization opportunities.

In this paper, we propose, to the best of our knowledge, the first algorithm for the automatic synthesis of preconditions for compiler optimizations. The synthesized preconditions are provably correct by construction, and they are guaranteed to be the weakest in the precondition language that we consider.

We implemented the proposed technique in a tool named PSyCO. We present examples of preconditions synthesized by PSyCO, as well as the results of running PSyCO on a set of optimizations.

References

[1]

Aho, A.V., Lam, M.S., Sethi, R., Ullman, J.D.: Compilers: Principles, Techniques, and Tools, 2nd edn. Addison-Wesley 2006

Digital Library

[2]

Bansal, S., Aiken, A.: Automatic generation of peephole superoptimizers. In: ASPLOS 2006

Digital Library

[3]

Barthe, G., Crespo, J.M., Kunz, C.: Relational verification using product programs. In: Butler, M., Schulte, W. eds. FM 2011. LNCS, vol. 6664, pp. 200---214. Springer, Heidelberg 2011

Digital Library

[4]

Benton, N.: Simple relational correctness proofs for static analyses and program transformations. In: POPL 2004

Digital Library

[5]

Bozga, M., Iosif, R., Koneă ný, F.: Deciding conditional termination. In: Flanagan, C., König, B. eds. TACAS 2012. LNCS, vol. 7214, pp. 252---266. Springer, Heidelberg 2012

Digital Library

[6]

Brain, M., Crick, T., De Vos, M., Fitch, J.: TOAST: Applying answer set programming to superoptimisation. In: Etalle, S., Truszczyński, M. eds. ICLP 2006. LNCS, vol. 4079, pp. 270---284. Springer, Heidelberg 2006

Digital Library

[7]

Calcagno, C., Distefano, D., O'Hearn, P., Yang, H.: Compositional shape analysis by means of bi-abduction. In: POPL 2009

Digital Library

[8]

Cook, B., Gulwani, S., Lev-Ami, T., Rybalchenko, A., Sagiv, M.: Proving conditional termination. In: Gupta, A., Malik, S. eds. CAV 2008. LNCS, vol. 5123, pp. 328---340. Springer, Heidelberg 2008

Digital Library

[9]

Cousot, P., Cousot, R., Fähndrich, M., Logozzo, F.: Automatic inference of necessary preconditions. In: Giacobazzi, R., Berdine, J., Mastroeni, I. eds. VMCAI 2013. LNCS, vol. 7737, pp. 128---148. Springer, Heidelberg 2013

Digital Library

[10]

de Moura, L., BjØrner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. eds. TACAS 2008. LNCS, vol. 4963, pp. 337---340. Springer, Heidelberg 2008

Digital Library

[11]

Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM 188, 453---457 1975

Digital Library

[12]

Godlin, B., Strichman, O.: Inference rules for proving the equivalence of recursive procedures. Acta Inf. 456, 403---439 2008

Digital Library

[13]

Goldberg, B., Zuck, L., Barrett, C.: Into the loops: Practical issues in translation validation for optimizing compilers. Electron. Notes Theor. Comp. Sci. 132 2005

Digital Library

[14]

Gulwani, S., Jha, S., Tiwari, A., Venkatesan, R.: Synthesis of loop-free programs. In: PLDI 2011

Digital Library

[15]

Gulwani, S., Srivastava, S., Venkatesan, R.: Constraint-based invariant inference over predicate abstraction. In: Jones, N.D., Müller-Olm, M. eds. VMCAI 2009. LNCS, vol. 5403, pp. 120---135. Springer, Heidelberg 2009

Digital Library

[16]

Guo, S.-Y., Palsberg, J.: The essence of compiling with traces. In: POPL 2011

Digital Library

[17]

Hawblitzel, C., Kawaguchi, M., Lahiri, S.K., Rebêlo, H.: Towards modularly comparing programs using automated theorem provers. In: Bonacina, M.P. ed. CADE 2013. LNCS, vol. 7898, pp. 282---299. Springer, Heidelberg 2013

Digital Library

[18]

Joshi, R., Nelson, G., Zhou, Y.: Denali: A practical algorithm for generating optimal code. ACM Trans. Program. Lang. Syst. 286, 967---989 2006

Digital Library

[19]

Junker, U.: QUICKXPLAIN: Preferred explanations and relaxations for over-constrained problems. In: AAAI 2004

Digital Library

[20]

Kundu, S., Tatlock, Z., Lerner, S.: Proving optimizations correct using parameterized program equivalence. In: PLDI 2009

Digital Library

[21]

Leino, K.R.M.: Efficient weakest preconditions. Inf. Process. Lett. 936, 281---288 2005

Digital Library

[22]

Lerner, S., Millstein, T., Chambers, C.: Automatically proving the correctness of compiler optimizations. In: PLDI 2003

Digital Library

[23]

Lerner, S., Millstein, T., Rice, E., Chambers, C.: Automated soundness proofs for dataflow analyses and transformations via local rules. In: POPL 2005

Digital Library

[24]

Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 527, 107---115 2009

Digital Library

[25]

Lopes, N.P., Monteiro, J.: Automatic equivalence checking of UF+IA programs. In: Bartocci, E., Ramakrishnan, C.R. eds. SPIN 2013. LNCS, vol. 7976, pp. 282---300. Springer, Heidelberg 2013

[26]

Marques-Silva, J., Janota, M., Belov, A.: Minimal sets over monotone predicates in boolean formulae. In: Sharygina, N., Veith, H. eds. CAV 2013. LNCS, vol. 8044, pp. 592---607. Springer, Heidelberg 2013

[27]

Moy, Y.: Sufficient preconditions for modular assertion checking. In: Logozzo, F., Peled, D.A., Zuck, L.D. eds. VMCAI 2008. LNCS, vol. 4905, pp. 188---202. Springer, Heidelberg 2008

Digital Library

[28]

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

Digital Library

[29]

Namjoshi, K.S., Zuck, L.D.: Witnessing program transformations. In: Logozzo, F., Fähndrich, M. eds. SAS 2013. LNCS, vol. 7935, pp. 304---323. Springer, Heidelberg 2013

[30]

Necula, G.C.: Translation validation for an optimizing compiler. In: PLDI 2000

Digital Library

[31]

Pnueli, A., Siegel, M., Singerman, E.: Translation validation. In: Steffen, B. ed. TACAS 1998. LNCS, vol. 1384, pp. 151---166. Springer, Heidelberg 1998

Digital Library

[32]

Scherpelz, E.R., Lerner, S., Chambers, C.: Automatic inference of optimizer flow functions from semantic meanings. In: PLDI 2007

Digital Library

[33]

Seghir, M.N., Kroening, D.: Counterexample-guided precondition inference. In: Felleisen, M., Gardner, P. eds. ESOP 2013. LNCS, vol. 7792, pp. 451---471. Springer, Heidelberg 2013

Digital Library

[34]

Stepp, M., Tate, R., Lerner, S.: Equality-based translation validator for LLVM. In: Gopalakrishnan, G., Qadeer, S. eds. CAV 2011. LNCS, vol. 6806, pp. 737---742. Springer, Heidelberg 2011

Digital Library

[35]

Tate, R., Stepp, M., Tatlock, Z., Lerner, S.: Equality saturation: a new approach to optimization. In: POPL 2009

Digital Library

[36]

Tate, R., Stepp, M., Tatlock, Z., Lerner, S.: Generating compiler optimizations from proofs. In: POPL 2010

Digital Library

[37]

Tatlock, Z., Lerner, S.: Bringing extensibility to verified compilers. In: PLDI 2010

Digital Library

[38]

Tristan, J.-B., Govereau, P., Morrisett, G.: Evaluating value-graph translation validation for LLVM. In: PLDI 2011

Digital Library

[39]

Yang, X., Chen, Y., Eide, E., Regehr, J.: Finding and understanding bugs in C compilers. In: PLDI 2011

Digital Library

[40]

Zaks, A., Pnueli, A.: CoVaC: Compiler validation by program analysis of the cross-product. In: Cuellar, J., Sere, K. eds. FM 2008. LNCS, vol. 5014, pp. 35---51. Springer, Heidelberg 2008

Digital Library

[41]

Zhao, J., Nagarakatte, S., Martin, M.M., Zdancewic, S.: Formal verification of SSA-based optimizations for LLVM. In: PLDI 2013

Digital Library

[42]

Zuck, L., Pnueli, A., Goldberg, B., Barrett, C., Fang, Y., Hu, Y.: Translation and run-time validation of loop transformations. Form. Methods Syst. Des. 27 2005

Digital Library

Cited By

Newcomb JAdams AJohnson SBodik RKamil S(2020)Verifying and improving Halide’s term rewriting system with program synthesisProceedings of the ACM on Programming Languages10.1145/34282344:OOPSLA(1-28)Online publication date: 13-Nov-2020
https://dl.acm.org/doi/10.1145/3428234
Menendez DNagarakatte S(2017)Alive-Infer: data-driven precondition inference for peephole optimizations in LLVMACM SIGPLAN Notices10.1145/3140587.306237252:6(49-63)Online publication date: 14-Jun-2017
https://dl.acm.org/doi/10.1145/3140587.3062372
Menendez DNagarakatte SCohen AVechev M(2017)Alive-Infer: data-driven precondition inference for peephole optimizations in LLVMProceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/3062341.3062372(49-63)Online publication date: 14-Jun-2017
https://dl.acm.org/doi/10.1145/3062341.3062372
Show More Cited By

Recommendations

Source-Level Compiler Optimizations for High-Level Synthesis
SEEDA-CECNSM '16: Proceedings of the SouthEast European Design Automation, Computer Engineering, Computer Networks and Social Media Conference

With high-level synthesis becoming the preferred method for hardware design, tools that operate on high-level programming languages and optimize hardware output are crucial for successful synthesis. In high-level synthesis, conventional programming ...
Weakest precondition based verification tool that models spatial ordering

Weakest precondition based method for specification and verification of geographically distributed system is described. For this purpose spatial predicates have been defined. A distributed mutual exclusion algorithm is proposed and is used to illustrate ...
Efficient Self-composition for Weakest Precondition Calculi
Proceedings of the 19th International Symposium on FM 2014: Formal Methods - Volume 8442

This paper contributes to deductive verification of language based secure information flow. A popular approach in this area is self-composition in combination with off-the-shelf software verification systems to check for secure information flow. This ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

VMCAI 2014: Proceedings of the 15th International Conference on Verification, Model Checking, and Abstract Interpretation - Volume 8318

January 2014

491 pages

ISBN:9783642540127

Editors:
Kenneth Mcmillan
One Microsoft Way, Microsoft Research, Redmond, USA
,
Xavier Rival
DI - Ecole Normale Supérieure, Paris Cedex 05, France

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 19 January 2014

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

8
Total Citations
View Citations
0
Total Downloads

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

Reflects downloads up to 18 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Newcomb JAdams AJohnson SBodik RKamil S(2020)Verifying and improving Halide’s term rewriting system with program synthesisProceedings of the ACM on Programming Languages10.1145/34282344:OOPSLA(1-28)Online publication date: 13-Nov-2020
https://dl.acm.org/doi/10.1145/3428234
Menendez DNagarakatte S(2017)Alive-Infer: data-driven precondition inference for peephole optimizations in LLVMACM SIGPLAN Notices10.1145/3140587.306237252:6(49-63)Online publication date: 14-Jun-2017
https://dl.acm.org/doi/10.1145/3140587.3062372
Menendez DNagarakatte SCohen AVechev M(2017)Alive-Infer: data-driven precondition inference for peephole optimizations in LLVMProceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/3062341.3062372(49-63)Online publication date: 14-Jun-2017
https://dl.acm.org/doi/10.1145/3062341.3062372
Reynolds AKing TKuncak V(2017)Solving quantified linear arithmetic by counterexample-guided instantiationFormal Methods in System Design10.1007/s10703-017-0290-y51:3(500-532)Online publication date: 1-Dec-2017
https://dl.acm.org/doi/10.1007/s10703-017-0290-y
Lopes NMonteiro J(2016)Automatic equivalence checking of programs with uninterpreted functions and integer arithmeticInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-015-0366-118:4(359-374)Online publication date: 1-Aug-2016
https://dl.acm.org/doi/10.1007/s10009-015-0366-1
Peleg HShoham SYahav E(2016)$$D^3$$Proceedings of the 17th International Conference on Verification, Model Checking, and Abstract Interpretation - Volume 958310.1007/978-3-662-49122-5_9(185-205)Online publication date: 17-Jan-2016
https://dl.acm.org/doi/10.1007/978-3-662-49122-5_9
Lopes NMenendez DNagarakatte SRegehr J(2015)Provably correct peephole optimizations with aliveACM SIGPLAN Notices10.1145/2813885.273796550:6(22-32)Online publication date: 3-Jun-2015
https://dl.acm.org/doi/10.1145/2813885.2737965
Lopes NMenendez DNagarakatte SRegehr JGrove DBlackburn S(2015)Provably correct peephole optimizations with aliveProceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/2737924.2737965(22-32)Online publication date: 3-Jun-2015
https://dl.acm.org/doi/10.1145/2737924.2737965

View Options

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

Media

Figures

Other

Tables

View Table of Contents