Automatic inference of optimizer flow functions from semantic meanings

ABSTRACT

Previous work presented a language called Rhodium for writing program analyses and transformations, in the form of declarative flow functions that propagate instances of user-defined dataflow fact schemas. Each dataflow fact schema specifies a semantic meaning, which allows the Rhodium system to automatically verify the correctness of the user's flow functions. In this work, we have reversed the roles of the flow functions and semantic meanings: rather than checking the correctness of the user-written flow functions using the facts' semantic meanings, we automatically infer correct flow functions solely from the meanings of the dataflow fact schemas. We have implemented our algorithm for inferring flow functions from fact schemas in the context of the Whirlwind compiler, and have used this implementation to infer flow functions for a variety of fact schemas. The automatically generated flow functions cover most of the situations covered by an earlier suite of handwritten rules.

REFERENCES

• 1: J. M. Andreoli. Logic programming with focusing proofs in linear logic. Journal of Logic and Computation, 1992.
• 2: Thomas Ball , Rupak Majumdar , Todd Millstein , Sriram K. Rajamani, Automatic predicate abstraction of C programs, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.203-213, June 2001, Snowbird, Utah, United States
• 3: Robert Cartwright , Derek C. Oppen, The logic of aliasing, Stanford University, Stanford, CA, 1979
• 4: R. L. Constable , S. F. Allen , H. M. Bromley , W. R. Cleaveland , J. F. Cremer , R. W. Harper , D. J. Howe , T. B. Knoblock , N. P. Mendler , P. Panangaden , J. T. Sasaki , S. F. Smith, Implementing mathematics with the Nuprl proof development system, Prentice-Hall, Inc., Upper Saddle River, NJ, 1986
• 5: Patrick Cousot. Verification by abstract interpretation. In Verification Theory & Practice, volume 2772 of LNCS. Springer-Verlag, 2003.
• 6: Satyaki Das , David L. Dill , Seungjoon Park, Experience with Predicate Abstraction, Proceedings of the 11th International Conference on Computer Aided Verification, p.160-171, July 06-10, 1999
• 7: David Detlefs , Greg Nelson , James B. Saxe, Simplify: a theorem prover for program checking, Journal of the ACM (JACM), v.52 n.3, p.365-473, May 2005 [doi>10.1145/1066100.1066102]
• 8: M.J.C. Gordon. HOL: A proof generating system for higher-order logic. In VLSI Specification Verification and Synthesis. Kluwer Academic Publishers, 1988.
• 9: Susanne Graf , Hassen Saïdi, Construction of Abstract State Graphs with PVS, Proceedings of the 9th International Conference on Computer Aided Verification, p.72-83, June 22-25, 1997
• 10: David Gries, The Science of Programming, Springer-Verlag New York, Inc., Secaucus, NJ, 1987
• 11: Thomas A. Henzinger , Ranjit Jhala , Rupak Majumdar , Grégoire Sutre, Lazy abstraction, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.58-70, January 16-18, 2002, Portland, Oregon
• 12: M. Kauffmann and R. S. Boyer. The Boyer-Moore theorem prover and its interactive enhancement. Computers and Mathematics with Applications, 29(2), 1995.
• 13: Matt Kaufmann , J. Strother Moore , Panagiotis Manolios, Computer-Aided Reasoning: An Approach, Kluwer Academic Publishers, Norwell, MA, 2000
• 14: Shuvendu Lahiri, Thomas Ball, and Byron Cook. Predicate abstraction via symbolic decision procedures. In Computer Aided Verification (CAV), July 2005.
• 15: Sorin Lucian Lerner , Craig Chambers, Automatically proving the correctness of program analyses and transformations, University of Washington, Seattle, WA, 2006
• 16: Sorin Lerner , Todd Millstein , Craig Chambers, Automatically proving the correctness of compiler optimizations, Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation, June 09-11, 2003, San Diego, California, USA
• 17: Sorin Lerner , Todd Millstein , Erika Rice , Craig Chambers, Automated soundness proofs for dataflow analyses and transformations via local rules, Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.364-377, January 12-14, 2005, Long Beach, California, USA
• 18: Tal Lev-Ami , Shmuel Sagiv, TVLA: A System for Implementing Static Analyses, Proceedings of the 7th International Symposium on Static Analysis, p.280-301, June 29-July 01, 2000
• 19: Sam Owre , John M. Rushby , Natarajan Shankar, PVS: A Prototype Verification System, Proceedings of the 11th International Conference on Automated Deduction: Automated Deduction, p.748-752, June 15-18, 1992
• 20: L. C. Paulson. Isabelle: A generic theorem prover, volume 828 of LNCS. Springer-Verlag, 1994.
• 21: Frank Pfenning , Carsten Schürmann, System Description: Twelf - A Meta-Logical Framework for Deductive Systems, Proceedings of the 16th International Conference on Automated Deduction: Automated Deduction, p.202-206, July 07-10, 1999
• 22: John Regehr , Usit Duongsaa, Deriving abstract transfer functions for analyzing embedded software, Proceedings of the 2006 ACM SIGPLAN/SIGBED conference on Language, compilers, and tool support for embedded systems, June 14-16, 2006, Ottawa, Ontario, Canada
• 23: John Regehr , Alastair Reid, HOIST: a system for automatically deriving static analyzers for embedded systems, Proceedings of the 11th international conference on Architectural support for programming languages and operating systems, October 07-13, 2004, Boston, MA, USA
• 24: Thomas Reps, Mooly Sagiv, and Alexey Loginov. Finite differencing of logical formulas for static analysis. In European Symposium on Programming (ESOP), April 2003.
• 25: Thomas Reps, Mooly Sagiv, and Greta Yorsh. Symbolic implementation of the best transformer. In Verification, Model Checking, and Abstract Interpretation (VMCAI), January 2004.
• 26: Erika Rice, Sorin Lerner, and Craig Chambers. Automatically inferring sound dataflow functions from dataflow fact schemas. In Workshop on Compiler Optimization Meets Compiler Verification (COCV), April 2005.
• 27: Erika Rice, Sorin Lerner, and Craig Chambers. Automatic inference of dataflow analyses. Technical Report UW-CSE-2006-06-04, University of Washington, June 2006.
• 28: Carsten Schürmann , Frank Pfenning, Automated Theorem Proving in a Simple Meta-Logic for LF, Proceedings of the 15th International Conference on Automated Deduction: Automated Deduction, p.286-300, July 05-10, 1998
• 29: Greta Yorsh, Thomas Reps, and Mooly Sagiv. Symbolically computing most-precise abstract operations for shape analysis. In Tools and Algorithms for the Construction and Analysis of Systems(TACAS), March 2004.

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.4 Processors
          Subjects: Compilers

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.4 Processors
          Subjects: Optimization

General Terms:
Algorithms, Languages, Reliability