Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Cliff Click and Keith D. Cooper. Combining analyses, combining optimizations. ACM Transactions on Programming Languages and Systems, 17(2):181–196, March 1995.
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.
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.
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.
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.
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.
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.
Sorin Lerner, David Grove, and Craig Chambers. Composing dataflow analyses and transformations. A CM SIGPLAN Notices, 31(1):270–282, January 2002.
Steven S. Muchnick. Advanced Compiler Design and Implementation. Morgan Kaufmann, San Francisco, 2000.
Matthias Müller. Abstraction benchmarks and performance of C++ applications. In Proceedings of the Fourth International Conference on Supercomputing in Nuclear Applications, 2000.
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.
Amr Sabry and Matthias Felleisen. Reasoning about programs in continuation-passing style. LISP and Symbolic Computation, 6(3–4):289–360, 1993.
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.
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.
Alex Stepanov. Abstraction penalty benchmark, 1994.
Walid Taha and Tim Sheard. Multi-stage programming with explicit annotations. ACM SIGPLAN Notices, 32(12):203–217, 1997.
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.
Todd L. Veldhuizen and Andrew Lumsdaine. Guaranteed optimization: Proving nullspace properties of compilers. Technical Report TR564, Indiana University Computer Science, 2002.
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.
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).
P. Wadler. Deforestation: transforming programs to eliminate trees. Theoretical Computer Science, 73(2):231–248, June 1990.
Mark N. Wegman and Kenneth Zadeck. Constant propagation with conditional branches. ACM Transactions on Programming Languages and Systems, 13(2):181–210, April 1991.
Jiawang Wei. Correctness of fixpoint transformations. Theoretical Computer Science, 129(1):123–142, June 1994.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Veldhuizen, T.L., Lumsdaine, A. (2002). Guaranteed Optimization: Proving Nullspace Properties of Compilers. In: Hermenegildo, M.V., Puebla, G. (eds) Static Analysis. SAS 2002. Lecture Notes in Computer Science, vol 2477. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45789-5_20
Download citation
DOI: https://doi.org/10.1007/3-540-45789-5_20
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-44235-6
Online ISBN: 978-3-540-45789-3
eBook Packages: Springer Book Archive