The pitfalls of verifying floating-point computations

ABSTRACT

Current critical systems often use a lot of floating-point computations, and thus the testing or static analysis of programs containing floating-point operators has become a priority. However, correctly defining the semantics of common implementations of floating-point is tricky, because semantics may change according to many factors beyond source-code level, such as choices made by compilers. We here give concrete examples of problems that can appear and solutions for implementing in analysis software.

REFERENCES

• 1: Advanced Micro Devices. 2005. AMD64 Architecture Programmer's Manual Volume 1: Application Programming, 3.10 ed. Advanced Micro Devices.
• 2: Andrew W. Appel, Modern Compiler Implementation in C: Basic Techniques, Cambridge University Press, New York, NY, 1997
• 3: Balakrishnan, G. and Reps, T. W. 2004. Analyzing memory accesses in x86 executables. In Proceedings of the International Conference on Computer Construction. Lecture Notes in Computer Science, vol. 2985. Springer-Verlag, New York.
• 4: Bruno Blanchet , Patrick Cousot , Radhia Cousot , Jérôme Feret , Laurent Mauborgne , Antoine Miné , David Monniaux , Xavier Rival, Design and implementation of a special-purpose static program analyzer for safety-critical real-time embedded software, The essence of computation: complexity, analysis, transformation, Springer-Verlag New York, Inc., New York, NY, 2002
• 5: Bruno Blanchet , Patrick Cousot , Radhia Cousot , Jérome Feret , Laurent Mauborgne , Antoine Miné , David Monniaux , Xavier Rival, A static analyzer for large safety-critical software, Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation, June 09-11, 2003, San Diego, California, USA
• 6: P. Caspi , D. Pilaud , N. Halbwachs , J. A. Plaice, LUSTRE: a declarative language for real-time programming, Proceedings of the 14th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.178-188, January 21-23, 1987, Munich, West Germany [doi>10.1145/41625.41641]
• 7: William D. Clinger, How to read floating point numbers accurately, Proceedings of the ACM SIGPLAN 1990 conference on Programming language design and implementation, p.92-101, June 1990, White Plains, New York, United States
• 8: Thomas T. Cormen , Charles E. Leiserson , Ronald L. Rivest, Introduction to algorithms, MIT Press, Cambridge, MA, 1990
• 9: Cousot, P. 1997. Constructive design of a hierarchy of semantics of a transition system by abstract interpretation. Electronic Notes in Theoretical Computer Science 6, Elsevier, 77--102.
• 10: Patrick Coust, Methods and logics for proving programs, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
• 11: Patrick Cousot , Rahida Cousot, Abstract interpretation and application to logic programs, Journal of Logic Programming, v.13 n.2-3, p.103-179, July 1992 [doi>10.1016/0743-1066(92)90030-7]
• 12: Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., and Rival, X. 2005. The ASTRÉE analyzer. In European Symposium on Programming (ESOP). Lecture Notes in Computer Science, vol. 3444, Springer-Verlag, New York, 21--30.
• 13: Samuel Arturo Figueroa Del Cid , Robert B. Dewar, A rigorous framework for fully supporting the ieee standard for floating-point arithmetic in high-level programming languages, New York University, New York, NY, 2000
• 14: Sylvie Boldo , Jean-Christophe Filliatre, Formal Verification of Floating-Point Programs, Proceedings of the 18th IEEE Symposium on Computer Arithmetic, p.187-194, June 25-27, 2007 [doi>10.1109/ARITH.2007.20]
• 15: Free Software Foundation. 2005a. Documentation for gcj (gcc 4.1.1). Free Software Foundation, Boston, MA.
• 16: Free Software Foundation. 2005b. The GNU compiler collection. Free Software Foundation, Boston, MA.
• 17: Freescale Semiconductor, Inc. 2001a. MPC750 RISC Microprocessor Family User's Manual. Freescale Semiconductor, Inc. MPC750UM/D.
• 18: Freescale Semiconductor, Inc. 2001b. Programming Environments Manual for 32-Bit Implementations of the PowerPC Architecture. Freescale Semiconductor, Inc. MPCFPE32B/AD.
• 19: 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]
• 20: James Gosling , Bill Joy , Guy Steele , Gilad Bracha, Java(TM) Language Specification, The (3rd Edition) (Java (Addison-Wesley)), Addison-Wesley Professional, 2005
• 21: James Gosling , Bill Joy , Guy L. Steele, The Java Language Specification, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1996
• 22: James Gosling , Bill Joy , Guy Steele , Gilad Bracha, Java Language Specification, Second Edition: The Java Series, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 2000
• 23: 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
• 24: C. A. R. Hoare, An axiomatic basis for computer programming, Communications of the ACM, v.12 n.10, p.576-580, Oct. 1969 [doi>10.1145/363235.363259]
• 25: IEC 1989. International Standard—Binary Floating-Point Arithmetic for Microprocessor Systems, 2nd ed. IEC. IEC-60559.
• 26: IEEE 1985. IEEE Standard for Binary Floating-Point Arithmetic for Microprocessor Systems. IEEE. ANSI/IEEE Std 754-1985.
• 27: Intel Corp. 1997. Intel Architecture Software Developer's Manual Volume 1: Basic Architecture. Intel Corp. order number 243190.
• 28: Intel Corp. 2005. IA-32 Intel Architecture Software Developer's Manual Volume 1: Basic Architecture. Intel Corp. order number 253665-017.
• 29: ISO/IEC 1999. International Standard—Programming Languages—C. ISO/IEC 9899:1999.
• 30: Java Grande Forum Panel. 1998. Java grande forum report: Making java work for high-end computing. http://www.javagrande.org/sc98/sc98grande.pdf.
• 31: Kahan, W. 1987. Branch cuts for complex elementary functions, or much ado about nothing's sign bit. In The State of the Art in Numerical Analysis, A. Iserles and M. Powell, Eds. Clarendon Press, Oxford, UK, 165--211.
• 32: Kahan, W. and Darcy, J. D. 1998. How Java's floating-point hurts everyone everywhere. http://www.cs.berkeley.edu/~wkahan/JAVAhurt.pdf.
• 33: Leroy, X., Doligez, D., Garrigue, J., Rémy, D., and Vouillon, J. 2005. The Objective Caml System Release 3.09: Documentation and user's manual. INRIA.
• 34: Lions, J.-L., Lbeck, L., Fauquembergue, J.-L., Kahn, G., Kubbat, W., Levedag, S., Mazzini, L., Merle, D., and O'Halloran C. 1996. Ariane 5: Flight 501 failure, report by the inquiry board. Tech. rep., European Space Agency (ESA) and Centre national d'études spatiales (CNES).
• 35: T. Lynch , A. Ahmed , M. Schulte , T. Callaway , R. Tisdale, The K5 transcendental functions, Proceedings of the 12th Symposium on Computer Arithmetic, p.163, July 19-21, 1995
• 36: 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
• 37: Matthieu Martel, Static Analysis of the Numerical Stability of Loops, Proceedings of the 9th International Symposium on Static Analysis, p.133-150, September 17-20, 2002
• 38: 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]
• 39: Antoine Miné, The Octagon Abstract Domain, Proceedings of the Eighth Working Conference on Reverse Engineering (WCRE'01), p.310, October 02-05, 2001
• 40: Miné, A. 2004a. Domaines numériques abstraits faiblement relationnels. Ph.D. dissertation, École polytechnique.
• 41: Miné, A. 2004b. Relational abstract domains for the detection of floating-point run-time errors. In European Symposium on Programming (ESOP). Lecture Notes in Computer Science, vol. 2986, Springer-Verlag, New York, 3--17.
• 42: Muller, J.-M. 2005. On the definition of ulp(x). Tech. Rep. 2005-09, École normale supérieure de Lyon - Laboratoire de l'Informatique du Parallélisme.
• 43: Rice, H. G. 1953. Classes of recursively enumerable sets and their decision problems. Trans. Amer. Math. Soc. 74, 2 (Mar.), 358--366.
• 44: Xavier Rival, Abstract Interpretation-Based Certification of Assembly Code, Proceedings of the 4th International Conference on Verification, Model Checking, and Abstract Interpretation, p.41-55, January 09-11, 2002
• 45: Hartley Rogers, Jr., Theory of recursive functions and effective computability, MIT Press, Cambridge, MA, 1987
• 46: Guy L. Steele, Jr. , Jon L. White, How to print floating-point numbers accurately, Proceedings of the ACM SIGPLAN 1990 conference on Programming language design and implementation, p.112-126, June 1990, White Plains, New York, United States
• 47: Sun Microsystems. 2001. Numerical Computation Guide. Sun Microsystems, Inc., Santa Clara, CA.
• 48: Weisstein, E. W. 2005. Continued fraction. MathWorld, http://mathworld.wolfram.com.
• 49: Glynn Winskel, The formal semantics of programming languages: an introduction, MIT Press, Cambridge, MA, 1993

INDEX TERMS

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

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Mechanical verification
      F.3.2 Semantics of Programming Languages
          Subjects: Program analysis

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

Keywords:
AMD64, Abstract interpretation, Embedded software, FPU, Floating point, IA32, IEEE-754, PowerPC, Program testing, Rounding, Safety-Critical Software, Static analysis, Verification, x87