Program transformation for numerical precision

ABSTRACT

This article introduces a new program transformation in order to enhance the numerical accuracy of floating-point computations. We consider that a program would return an exact result if the computations were carried out using real numbers. In practice, roundoff errors due to the finite representation of values arise during the execution. These errors are closely related to the way formulas are evaluated. Indeed, mathematically equivalent formulas, obtained using laws like associativity, distributivity, etc., may lead to very different numerical results in the computer arithmetic. We propose a semantics-based transformation in order to optimize the numerical accuracy of programs. This transformation is expressed in the abstract interpretation framework and it aims at rewriting pieces of numerical codes in order to obtain results closer to what the computer would output if it used the exact arithmetic.

REFERENCES

• 1: ANSI/IEEE. IEEE Standard for Binary Floating-point Arithmetic, std 754-1985 edition, 1985.
• 2: David F. Bacon , Susan L. Graham , Oliver J. Sharp, Compiler transformations for high-performance computing, ACM Computing Surveys (CSUR), v.26 n.4, p.345-420, Dec. 1994 [doi>10.1145/197405.197406]
• 3: Christian H. Bischof , Paul D. Hovland , Boyana Norris, Implementation of automatic differentiation tools, Proceedings of the 2002 ACM SIGPLAN workshop on Partial evaluation and semantics-based program manipulation, January 14-15, 2002, Portland, Oregon
• 4: Martine Ceberio , Vladik Kreinovich, Greedy algorithms for optimizing multivariate Horner schemes, ACM SIGSAM Bulletin, v.38 n.1, March 2004 [doi>10.1145/980175.980179]
• 5: 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]
• 6: 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
• 7: Mila Dalla Preda , Roberto Giacobazzi, Control Code Obfuscation by Abstract Interpretation, Proceedings of the Third IEEE International Conference on Software Engineering and Formal Methods, p.301-310, September 07-09, 2005 [doi>10.1109/SEFM.2005.13]
• 8: David Goldberg, What every computer scientist should know about floating-point arithmetic, ACM Computing Surveys (CSUR), v.23 n.1, p.5-48, March 1991 [doi>10.1145/103162.103163]
• 9: Eric Goubault, Static Analyses of the Precision of Floating-Point Operations, Proceedings of the 8th International Symposium on Static Analysis, p.234-259, July 16-18, 2001
• 10: Eric Goubault , Matthieu Martel , Sylvie Putot, Asserting the Precision of Floating-Point Computations: A Simple Abstract Interpreter, Proceedings of the 11th European Symposium on Programming Languages and Systems, p.209-212, April 08-12, 2002
• 11: E. Goubault, M. Martel, and S. Putot. Some future challenges in the validation of control systems. In Proceedings of the European Congress on Embedded Real Time Software (ERTS'06), 2006.
• 12: Neil D. Jones , Carsten K. Gomard , Peter Sestoft, Partial evaluation and automatic program generation, Prentice-Hall, Inc., Upper Saddle River, NJ, 1993
• 13: Philippe Langlois , Nicolas Louvet, How to Ensure a Faithful Polynomial Evaluation with the Compensated Horner Algorithm, Proceedings of the 18th IEEE Symposium on Computer Arithmetic, p.141-149, June 25-27, 2007 [doi>10.1109/ARITH.2007.21]
• 14: Information Management and Technology Division. Patriot missile defense : Software problem led to system failure in Dhahran, saudi arabia. Technical Report B-247-094, United State General Accounting Office, 1992.
• 15: Matthieu Martel, Propagation of Roundoff Errors in Finite Precision Computations: A Semantics Approach, Proceedings of the 11th European Symposium on Programming Languages and Systems, p.194-208, April 08-12, 2002
• 16: M. Martel. An overview of semantics for the validation of numerical programs. In Verification, Model Checking and Abstract Interpretation, VMCAI'05, number 3385 in Lecture Notes in Computer Science, pages 59--77. Springer-Verlag, 2005.
• 17: Matthieu Martel, Semantics of roundoff error propagation in finite precision calculations, Higher-Order and Symbolic Computation, v.19 n.1, p.7-30, March 2006 [doi>10.1007/s10990-006-8608-2]
• 18: M. Martel. Semantics-based transformation of arithmetic expressions. In Static Analysis Symposium, SAS'07, number 4634 in Lecture Notes in Computer Science. Springer-Verlag, 2007.
• 19: M. Martel. Enhancing the implementation of mathematical formulas for fixed-point and floating-point arithmetics. In First International Workshop on Numerical Abstractions for Software Verification, NSV'08, 2008.
• 20: David Monniaux, The pitfalls of verifying floating-point computations, ACM Transactions on Programming Languages and Systems (TOPLAS), v.30 n.3, p.1-41, May 2008 [doi>10.1145/1353445.1353446]
• 21: Romuald Rocher , Daniel Menard , Nicolas Herve , Olivier Sentieys, Fixed-point configurable hardware components, EURASIP Journal on Embedded Systems, v.2006 n.1, p.20-20, January 2006 [doi>10.1155/ES/2006/23197]
• 22: R. Rocher, D. Menard, O. Sentieys, and P. Scalart. Analytical accuracy evaluation of fixed-point systems. In EUSIPCO'07Poznan, Pologne, 2007.
• 23: P. H. Sterbenz. Floating-point Computation. Prentice Hall International, 1974.

INDEX TERMS

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

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

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Program analysis

  G. Mathematics of Computing
  G.1 NUMERICAL ANALYSIS
      G.1.0 General
          Subjects: Computer arithmetic

General Terms:
Algorithms, Languages, Theory, Verification

Keywords:
abstract interpretation, compiler optimizations, floating-point numbers, numerical precision, program transformation