Guaranteed Optimization: Proving Nullspace Properties of Compilers

  • Todd L. Veldhuizen
  • Andrew Lumsdaine
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2477)


Writing performance-critical programs can be frustrating because optimizing compilers for imperative languages tend to be unpredictable. For a subset of optimizations - those that simplify rather than reorder code - it would be useful to prove that a compiler reliably performs optimizations. We show that adopting a “superanalysis” approach to optimization enables such a proof. By analogy with linear algebra, we define the nullspace of an optimizer as those programs it reduces to the empty program. To span the nullspace, we define rewrite rules that de-optimize programs by introducing abstraction. For a model compiler we prove that any sequence of de-optimizing rewrite rule applications is undone by the optimizer. Thus, we are able to give programmers a clear mental model of what simplifications the compiler is guaranteed to perform, and make progress on the problem of “abstraction penalty” in imperative languages.


Analysis Equation Program Language Proof Technique Functional Program Rule Application 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Cliff Click and Keith D. Cooper. Combining analyses, combining optimizations. ACM Transactions on Programming Languages and Systems, 17(2):181–196, March 1995.Google Scholar
  2. 2.
    Patrick Cousot and Radhia Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proc. Principles of Programming Languages, pages 238–252, January 1977.Google Scholar
  3. 3.
    Patrick Cousot and Radhia Cousot. Automatic synthesis of optimal invariant assertions: Mathematical foundations. In Proceedings of the 1977 symposium on Artificial intelligence and programming languages, pages 1–12, 1977.Google Scholar
  4. 4.
    Nachum Dershowitz. A taste of rewrite systems. In Proc. Functional Programming, Concurrency, Simulation and Automated Reasoning, volume 693 of Lecture Notes in Computer Science, pages 199–228, 1993.Google Scholar
  5. 5.
    Nachum Dershowitz and Jean-Pierre Jouannaud. Rewrite systems. In Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (B), pages 243–320. 1990.Google Scholar
  6. 6.
    A. J. Gill and S. L. Peyton Jones. Cheap deforestation in practice: An optimiser for Haskell. In Bjørn Pehrson and Imre Simon, editors, Proceedings of the IFIP 13th World Computer Congress. Volume 1: Technology and Foundations, pages 581–586, Amsterdam, The Netherlands, August 28–September 1 1994. Elsevier Science Publishers.Google Scholar
  7. 7.
    Gary A. Kildall. A unified approach to global program optimization. In Conference Record of the ACM Symposium on Principles of Programming Languages, pages 194–206. ACM SIGACT and SIGPLAN, ACM Press, 1973.Google Scholar
  8. 8.
    Sorin Lerner, David Grove, and Craig Chambers. Composing dataflow analyses and transformations. A CM SIGPLAN Notices, 31(1):270–282, January 2002.Google Scholar
  9. 9.
    Steven S. Muchnick. Advanced Compiler Design and Implementation. Morgan Kaufmann, San Francisco, 2000.Google Scholar
  10. 10.
    Matthias Müller. Abstraction benchmarks and performance of C++ applications. In Proceedings of the Fourth International Conference on Supercomputing in Nuclear Applications, 2000.Google Scholar
  11. 11.
    Arch D. Robison. The abstraction penalty for small objects in C++. In POOMA’96: The Parallel Object-Oriented Methods and Applications Conference, Feb. 28–Mar. 1 1996. Santa Fe, New Mexico.Google Scholar
  12. 12.
    Amr Sabry and Matthias Felleisen. Reasoning about programs in continuation-passing style. LISP and Symbolic Computation, 6(3–4):289–360, 1993.CrossRefGoogle Scholar
  13. 13.
    David Sands. Total correctness by local improvement in the transformation of functional programs. ACM Transactions on Programming Languages and Systems, 18(2):175–234, March 1996.Google Scholar
  14. 14.
    Jeremy G. Siek and Andrew Lumsdaine. The matrix template library: A unifying framework for numerical linear algebra. In Parallel Object Oriented Scientific Computing. ECOOP, 1998.Google Scholar
  15. 15.
    Alex Stepanov. Abstraction penalty benchmark, 1994.Google Scholar
  16. 16.
    Walid Taha and Tim Sheard. Multi-stage programming with explicit annotations. ACM SIGPLAN Notices, 32(12):203–217, 1997.CrossRefGoogle Scholar
  17. 17.
    Todd L. Veldhuizen. Arrays in Blitz++. In Computing in Object-Oriented Parallel Environments: Second International Symposium (ISCOPE 98), volume 1505 of Lecture Notes in Computer Science, pages 223–230. Springer-Verlag, 1998.CrossRefGoogle Scholar
  18. 18.
    Todd L. Veldhuizen and Andrew Lumsdaine. Guaranteed optimization: Proving nullspace properties of compilers. Technical Report TR564, Indiana University Computer Science, 2002.Google Scholar
  19. 19.
    Eelco Visser. A survey of rewriting strategies in program transformation systems. In B. Gramlich and S. Lucas, editors, Workshop on Reduction Strategies in Rewriting and Programming (WRS’01), volume 57 of Electronic Notes in Theoretical Computer Science, Utrecht, The Netherlands, May 2001. Elsevier Science Publishers.Google Scholar
  20. 20.
    Eelco Visser, Zine-el-Abidine Benaissa, and Andrew Tolmach. Building program optimizers with rewriting strategies. ACM SIGPLAN Notices, 34(1):13–26, January 1999. Proceedings of the International Conference on Functional Programming (ICFP’98).Google Scholar
  21. 21.
    P. Wadler. Deforestation: transforming programs to eliminate trees. Theoretical Computer Science, 73(2):231–248, June 1990.Google Scholar
  22. 22.
    Mark N. Wegman and Kenneth Zadeck. Constant propagation with conditional branches. ACM Transactions on Programming Languages and Systems, 13(2):181–210, April 1991.Google Scholar
  23. 23.
    Jiawang Wei. Correctness of fixpoint transformations. Theoretical Computer Science, 129(1):123–142, June 1994.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Todd L. Veldhuizen
    • 1
  • Andrew Lumsdaine
    • 1
  1. 1.Indiana UniversityBloomingtonUSA

Personalised recommendations