Automated soundness proofs for dataflow analyses and transformations via local rules

ABSTRACT

We present Rhodium, a new language for writing compiler optimizations that can be automatically proved sound. Unlike our previous work on Cobalt, Rhodium expresses optimizations using explicit dataflow facts manipulated by local propagation and transformation rules. This new style allows Rhodium optimizations to be mutually recursively defined, to be automatically composed, to be interpreted in both flow-sensitive and -insensitive ways, and to be applied interprocedurally given a separate context-sensitivity strategy, all while retaining soundness. Rhodium also supports infinite analysis domains while guaranteeing termination of analysis. We have implemented a soundness checker for Rhodium and have specified and automatically proven the soundness of all of Cobalt's optimizations plus a variety of optimizations not expressible in Cobalt, including Andersen's points-to analysis, arithmetic-invariant detection, loop-induction-variable strength reduction, and redundant array load elimination.

REFERENCES

• 1: Kamal Aboul-Hosn and Dexter Kozen. KAT-ML: An interactive theorem prover for kleene algebra with tests. In Proceedings of the 4th International Workshop on the Implementation of Logics (WIL'03), University of Manchester, September 2003.
• 2: Jonathan Aldrich , Craig Chambers , Emin Gün Sirer , Susan J. Eggers, Static Analyses for Eliminating Unnecessary Synchronization from Java Programs, Proceedings of the 6th International Symposium on Static Analysis, p.19-38, September 22-24, 1999
• 3: L. O. Andersen. Program Analysis and Specialization for the C Programming Languge. PhD thesis, DIKU, University of Copenhagen, May 1994 (available as DIKU technical report 94-19).
• 4: Nick Benton, Simple relational correctness proofs for static analyses and program transformations, Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.14-25, January 14-16, 2004, Venice, Italy
• 5: Marc Berndl , Ondrej Lhoták , Feng Qian , Laurie Hendren , Navindra Umanee, Points-to analysis using BDDs, Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation, June 09-11, 2003, San Diego, California, USA
• 6: David Cachera, Thomas Jensen, David Pichardie, and Vlad Rusu. Extracting a data flow analyser in constructive logic. In Proceedings of the 13th European Symposium on Programming (ESOP 2004), volume 2986 of Lecture Notes in Computer Science. Springer-Verlag, 2004.
• 7: Craig Chambers, Jeffrey Dean, and David Grove. Frameworks for intra- and interprocedural dataflow analysis. Technical Report UW-CSE-96-11-02, University of Washington, November 1996.
• 8: Patrick Cousot , Radhia Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.238-252, January 17-19, 1977, Los Angeles, California [doi>10.1145/512950.512973]
• 9: Patrick Cousot , Radhia Cousot, Systematic design of program analysis frameworks, Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.269-282, January 29-31, 1979, San Antonio, Texas [doi>10.1145/567752.567778]
• 10: Patrick Cousot , Radhia Cousot, Systematic design of program transformation frameworks by abstract interpretation, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.178-190, January 16-18, 2002, Portland, Oregon
• 11: Jeffrey Dean , Greg DeFouw , David Grove , Vassily Litvinov , Craig Chambers, Vortex: an optimizing compiler for object-oriented languages, Proceedings of the 11th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.83-100, October 06-10, 1996, San Jose, California, United States
• 12: Cormac Flanagan , K. Rustan M. Leino , Mark Lillibridge , Greg Nelson , James B. Saxe , Raymie Stata, Extended static checking for Java, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 13: David Grove , Craig Chambers, A framework for call graph construction algorithms, ACM Transactions on Programming Languages and Systems (TOPLAS), v.23 n.6, p.685-746, November 2001 [doi>10.1145/506315.506316]
• 14: Joshua D. Guttman , John D. Ramsdell , Vipin Swarup, The VLISP verified Scheme system, Lisp and Symbolic Computation, v.8 n.1-2, p.33-110, March 1995 [doi>10.1007/BF01128407]
• 15: M. Kauffmann and R.S. Boyer. The Boyer-Moore theorem prover and its interactive enhancement. Computers and Mathematics with Applications, 29(2):27--62, 1995.
• 16: Dexter Kozen, Kleene algebra with tests, ACM Transactions on Programming Languages and Systems (TOPLAS), v.19 n.3, p.427-443, May 1997 [doi>10.1145/256167.256195]
• 17: David Lacey , Neil D. Jones , Eric Van Wyk , Carl Christian Frederiksen, Proving correctness of compiler optimizations by temporal logic, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.283-294, January 16-18, 2002, Portland, Oregon
• 18: Sorin Lerner , David Grove , Craig Chambers, Composing dataflow analyses and transformations, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.270-282, January 16-18, 2002, Portland, Oregon
• 19: 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
• 20: Sorin Lerner, Todd Millstein, Erika Rice, and Craig Chambers. Automated soundness proofs for dataflow analyses and transformations via local rules. Technical Report UW-CSE-2004-07-04, University of Washington, July 2004.
• 21: Greg Morrisett, Karl Crary, Neal Glew, Dan Grossman, Richard Samuels, Frederick Smith, David Walker, Stephanie Weirich, and Steve Zdancewic. TALx86: A realistic typed assembly language. In 1999 ACM SIGPLAN Workshop on Compiler Support for System Software, pages 25--35, Atlanta GA, May 1999.
• 22: George C. Necula, Proof-carrying code, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.106-119, January 15-17, 1997, Paris, France [doi>10.1145/263699.263712]
• 23: George C. Necula, Translation validation for an optimizing compiler, Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation, p.83-94, June 18-21, 2000, Vancouver, British Columbia, Canada
• 24: George C. Necula , Peter Lee, The design and implementation of a certifying compiler, Proceedings of the ACM SIGPLAN 1998 conference on Programming language design and implementation, p.333-344, June 17-19, 1998, Montreal, Quebec, Canada
• 25: Amir Pnueli , Michael Siegel , Eli Singerman, Translation Validation, Proceedings of the 4th International Conference on Tools and Algorithms for Construction and Analysis of Systems, p.151-166, March 28-April 04, 1998
• 26: Martin Rinard and Darko Marinov. Credible compilation. In Proceedings of the FLoC Workshop Run-Time Result Verification, July 1999.
• 27: Micha Sharir and Amir Pnueli. Two approaches to interprocedural data flow analysis. In Steven~S. Muchnick and Neil~D. Jones, editors, Program Flow Analysis: Theory and Applications, chapter 7, pages 189--233. Prentice-hall, 1981.
• 28: O. Shivers, Control flow analysis in scheme, Proceedings of the ACM SIGPLAN 1988 conference on Programming Language design and Implementation, p.164-174, June 20-24, 1988, Atlanta, Georgia, United States
• 29: Ganesh Sittampalam , Oege de Moor , Ken Friis Larsen, Incremental execution of transformation specifications, Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.26-38, January 14-16, 2004, Venice, Italy
• 30: Bernhard Steffen, Data Flow Analysis as Model Checking, Proceedings of the International Conference on Theoretical Aspects of Computer Software, p.346-365, September 24-27, 1991
• 31: D. Tarditi , G. Morrisett , P. Cheng , C. Stone , R. Harper , P. Lee, TIL: a type-directed optimizing compiler for ML, Proceedings of the ACM SIGPLAN 1996 conference on Programming language design and implementation, p.181-192, May 21-24, 1996, Philadelphia, Pennsylvania, United States
• 32: Steven W. K. Tjiang , John L. Hennessy, Sharlit—a tool for building optimizers, Proceedings of the ACM SIGPLAN 1992 conference on Programming language design and implementation, p.82-93, June 15-19, 1992, San Francisco, California, United States
• 33: Jeffrey D. Ullman, Principles of database and knowledge-base systems, Vol. I, Computer Science Press, Inc., New York, NY, 1988
• 34: John Whaley , Monica S. Lam, Cloning-based context-sensitive pointer alias analysis using binary decision diagrams, Proceedings of the ACM SIGPLAN 2004 conference on Programming language design and implementation, June 09-11, 2004, Washington DC, USA
• 35: Deborah L. Whitfield , Mary Lou Soffa, An approach for exploring code improving transformations, ACM Transactions on Programming Languages and Systems (TOPLAS), v.19 n.6, p.1053-1084, Nov. 1997 [doi>10.1145/267959.267960]
• 36: Kwangkeun Yi , Williams Ludwell Harrison, III, Automatic generation and management of interprocedural program analyses, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.246-259, March 1993, Charleston, South Carolina, United States [doi>10.1145/158511.158642]
• 37: William D. Young, A mechanically verified code generator, Journal of Automated Reasoning, v.5 n.4, p.493-518, Dec. 1989

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Correctness proofs

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Validation; Reliability
  D.3 PROGRAMMING LANGUAGES
      D.3.4 Processors
          Subjects: Optimization; Compilers

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Mechanical verification

General Terms:
Languages, Reliability, Verification

Keywords:
automated correctness proofs, compiler optimization