research-article

Open access

The pitfalls of verifying floating-point computations

Author:

David MonniauxAuthors Info & Claims

ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 30, Issue 3

Article No.: 12, Pages 1 - 41

https://doi.org/10.1145/1353445.1353446

Published: 21 May 2008 Publication History

PDF eReader

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.]]

Google Scholar

[2]

Appel, A. and Ginsburg, M. 1997. Modern Compiler Implementation in C, revised and expanded ed. Cambridge University Press, Cambridge, MA.]]

Digital Library

Google Scholar

[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.]]

Google Scholar

[4]

Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., and Rival, X. 2002. Design and implementation of a special-purpose static program analyzer for safety-critical real-time embedded software. In The Essence of Computation: Complexity, Analysis, Transformation. Lecture Notes in Computer Science, vol. 2566. Springer-Verlag, New York, 85--108.]]

Digital Library

Google Scholar

[5]

Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., and Rival, X. 2003. A static analyzer for large safety-critical software. In Proceedings of the Conference on Programming Language Design and Implementation. ACM, New York, 196--207.]]

Digital Library

Google Scholar

[6]

Caspi, P., Pilaud, D., Halbwachs, N., and Plaice, J. A. 1987. LUSTRE: A declarative language for real-time programming. In POPL '87: Proceedings of the 14th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages. ACM, New York, 178--188.]]

Digital Library

Google Scholar

[7]

Clinger, W. D. 1990. How to read floating point numbers accurately. In Proceedings of the Conference on Programming Language Design and Implementation. ACM, New York, 92--101.]]

Digital Library

Google Scholar

[8]

Cormen, T. H., Leiserson, C. E., and Rivest, R. L. 1990. Introduction to algorithms. MIT Press, Cambridge, MA.]]

Digital Library

Google Scholar

[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.]]

Google Scholar

[10]

Cousot, P. 1990. Methods and logics for proving programs. In Handbook of Theoretical Computer Science, J. van Leeuwen, Ed. Vol. B. MIT Press, Cambridge, MA, 841--994. Chapter 15.]]

Digital Library

Google Scholar

[11]

Cousot, P. and Cousot, R. 1992. Abstract interpretation and application to logic programs. J. Logic Prog. 2-3, 13, 103--179.]]

Digital Library

Google Scholar

[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.]]

Digital Library

Google Scholar

[13]

Figueroa del Cid, S. A. 2000. A rigorous framework for fully supporting the IEEE standard for floating-point arithmetic in high-level programming languages. Ph.D. thesis, New York University.]]

Digital Library

Google Scholar

[14]

Filliâtre, J.-C. and Boldo, S. 2007. Formal verification of floating-point programs. In ARITH 18: Proceedings of the 18th Annual IEEE Symposium on Computer Arithmetics. IEEE Computer Society Press, Los Alamitos, CA.]]

Digital Library

Google Scholar

[15]

Free Software Foundation. 2005a. Documentation for gcj (gcc 4.1.1). Free Software Foundation, Boston, MA.]]

Google Scholar

[16]

Free Software Foundation. 2005b. The GNU compiler collection. Free Software Foundation, Boston, MA.]]

Google Scholar

[17]

Freescale Semiconductor, Inc. 2001a. MPC750 RISC Microprocessor Family User's Manual. Freescale Semiconductor, Inc. MPC750UM/D.]]

Google Scholar

[18]

Freescale Semiconductor, Inc. 2001b. Programming Environments Manual for 32-Bit Implementations of the PowerPC Architecture. Freescale Semiconductor, Inc. MPCFPE32B/AD.]]

Google Scholar

[19]

Goldberg, D. 1991. What every computer scientist should know about floating-point arithmetic. ACM Comput. Surv. 23, 1, 5--48.]]

Digital Library

Google Scholar

[20]

Gosling, J., Joy, B., Steele, G., and Bracha, G. 2005. The Java Language Specification, Third ed. The Java Series. Addison-Wesley, Reading, MA.]]

Digital Library

Google Scholar

[21]

Gosling, J., Joy, B., and Steele, G. L. 1996. The Java Language Specification, 1st ed. Addison-Wesley, Reading, MA.]]

Digital Library

Google Scholar

[22]

Gosling, J., Joy, B., Steele, G. L., and Bracha, G. 2000. The Java Language Specification, 2nd ed. Addison-Wesley, Reading, MA.]]

Digital Library

Google Scholar

[23]

Goubault, E. 2001. Static analyzes of floating-point operations. In Proceedings of the International Static Analysis Symposium. Lecture Notes in Computer Science, vol. 2126, Springer-Verlag, New York.]]

Digital Library

Google Scholar

[24]

Hoare, C. A. R. 1969. An axiomatic basis for computer programming. Commun. ACM 12, 10, 576--580.]]

Digital Library

Google Scholar

[25]

IEC 1989. International Standard—Binary Floating-Point Arithmetic for Microprocessor Systems, 2nd ed. IEC. IEC-60559.]]

Google Scholar

[26]

IEEE 1985. IEEE Standard for Binary Floating-Point Arithmetic for Microprocessor Systems. IEEE. ANSI/IEEE Std 754-1985.]]

Google Scholar

[27]

Intel Corp. 1997. Intel Architecture Software Developer's Manual Volume 1: Basic Architecture. Intel Corp. order number 243190.]]

Google Scholar

[28]

Intel Corp. 2005. IA-32 Intel Architecture Software Developer's Manual Volume 1: Basic Architecture. Intel Corp. order number 253665-017.]]

Google Scholar

[29]

ISO/IEC 1999. International Standard—Programming Languages—C. ISO/IEC 9899:1999.]]

Google Scholar

[30]

Java Grande Forum Panel. 1998. Java grande forum report: Making java work for high-end computing. http://www.javagrande.org/sc98/sc98grande.pdf.]]

Google Scholar

[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.]]

Google Scholar

[32]

Kahan, W. and Darcy, J. D. 1998. How Java's floating-point hurts everyone everywhere. http://www.cs.berkeley.edu/~wkahan/JAVAhurt.pdf.]]

Google Scholar

[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.]]

Google Scholar

[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).]]

Google Scholar

[35]

Lynch, T., Ahmed, A., Schulte, M., Callaway, T., and Tisdale, R. 1995. The K5 transcendental functions. In ARITH-12: Proceedings of the 12th IEEE Symposium on Computer Arithmetic. IEEE Computer Society Press, Los Alamitos, CA, 163.]]

Digital Library

Google Scholar

[36]

Martel, M. 2002a. Propagation of roundoff errors in finite precision computations: A semantics approach. In ESOP. Lecture Notes in Computer Science, vol. 2305, Springer-Verlag, New York.]]

Digital Library

Google Scholar

[37]

Martel, M. 2002b. Static analysis of the numerical stability of loops. In Proceedings of the International Static Analysis Symposium. Lecture Notes in Computer Science, vol. 2477, Springer-Verlag, New York.]]

Digital Library

Google Scholar

[38]

Martel, M. 2006. Semantics of roundoff error propagation in finite precision computations. J. Higher Order and Symb. Computat. 19, 1, 7--30.]]

Digital Library

Google Scholar

[39]

Miné, A. 2001. The octagon abstract domain. In Proceedings of Working Conference on Reverse Engineering. IEEE Computer Society Press, Los Alamitos, CA, 310--319.]]

Digital Library

Google Scholar

[40]

Miné, A. 2004a. Domaines numériques abstraits faiblement relationnels. Ph.D. dissertation, École polytechnique.]]

Google Scholar

[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.]]

Google Scholar

[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.]]

Google Scholar

[43]

Rice, H. G. 1953. Classes of recursively enumerable sets and their decision problems. Trans. Amer. Math. Soc. 74, 2 (Mar.), 358--366.]]

Crossref

Google Scholar

[44]

Rival, X. 2003. Abstract interpretation-based certification of assembly code. In Proceedings of the Conference on Verification, Model Checking and Abstract Interpretation. Lecture Notes in Computer Science, vol. 2575. Springer-Verlag, New York, 41--55.]]

Digital Library

Google Scholar

[45]

Rogers, H. 1987. Theory of Recursive Functions and Effective Computability. MIT Press.]]

Digital Library

Google Scholar

[46]

Steele, G. L. and White, J. L. 1990. How to print floating-point numbers accurately. In Proceedings of the Conference on Programming Language Design and Implementation. ACM, New York, 112--126.]]

Digital Library

Google Scholar

[47]

Sun Microsystems. 2001. Numerical Computation Guide. Sun Microsystems, Inc., Santa Clara, CA.]]

Google Scholar

[48]

Weisstein, E. W. 2005. Continued fraction. MathWorld, http://mathworld.wolfram.com.]]

Google Scholar

[49]

Winskel, G. 1993. The Formal Semantics of Programming Languages: An Introduction. Foundations of Computing. MIT Press, Cambridge, MA.]]

Digital Library

Google Scholar

Cited By

View all

Kuhn LKlein BFröning H(2025)On the Non-associativity of Analog ComputationsMachine Learning and Principles and Practice of Knowledge Discovery in Databases10.1007/978-3-031-74643-7_15(183-195)Online publication date: 1-Jan-2025
https://doi.org/10.1007/978-3-031-74643-7_15
Chou YWu CJiang YKuo SKuo S(2024)Nanoscale Precision-Related Challenges in Classical and Quantum OptimizationIEEE Nanotechnology Magazine10.1109/MNANO.2024.337848818:3(31-43)Online publication date: Jun-2024
https://doi.org/10.1109/MNANO.2024.3378488
Konečný MPark SThies H(2024)Extracting efficient exact real number computation from proofs in constructive type theoryJournal of Logic and Computation10.1093/logcom/exae066Online publication date: 18-Oct-2024
https://doi.org/10.1093/logcom/exae066
Show More Cited By

Recommendations

The Floating-Point Unit of the Jaguar x86 Core
ARITH '13: Proceedings of the 2013 IEEE 21st Symposium on Computer Arithmetic

The AMD Jaguar x86 core uses a fully-synthesized, 128-bit native floating-point unit (FPU) built as a co-processor model. The Jaguar FPU supports several x86 ISA extensions, including x87, MMX, SSE1 through SSE4.2, AES, CLMUL, AVX, and F16C instruction ...
A Combined Interval and Floating Point Multiplier
GLS '98: Proceedings of the Great Lakes Symposium on VLSI '98

Interval arithmetic provides an efficient method for monitoring and controlling errors in numerical calculations. However, existing software packages for interval arithmetic are often too slow for numerically intensive computations. This paper presents ...
Redundant-Digit Floating-Point Addition Scheme Based on a Stored Rounding Value

Due to the widespread use and inherent complexity of floating-point addition, much effort has been devoted to its speedup via algorithmic and circuit techniques. We propose a new redundant-digit representation for floating-point numbers that leads to ...

Reviews

Reviewer: Bernard Kuc

Working within the quantitative analytics group of an investment bank, I see floating-point inconsistencies as an often-recurring problem. With any valuation or risk difference having to be explained and justified, releasing new versions of the analytics libraries is often a time consuming and problematic process. Hence, I was able to empathize with every floating-point problem mentioned in this paper. Monniaux starts with a description of the Institute of Electrical and Electronics Engineers (IEEE) floating-point standard, focusing on the aspects that can cause inconsistencies, such as optional portions of the standards, as well as the different operating and rounding modes of the floating-point processor. This is followed by a description of hardware differences. Monniaux explains, with easy-to-replicate example code, how the introduction of streaming single instruction multiple data (SIMD) extensions (SSE) instructions has affected the processing of floating-point numbers on the Intel architecture, showing how minor differences can result in faulty computations. Once the hardware problems have been explained, the next section covers compilers and how different compilers will produce different results with the same code fragment. Monniaux also covers the different optimizations available, including those introducing nonstandard behavior. He provides a complete C example that shows how different compilers and hardware architectures will produce significantly different results, before diverging into a brief discussion on the numerical issues that can occur in Java. The final section of the paper focuses on program validation. Monniaux shows how the challenges to define sound semantics make statistical analysis very difficult. Overall, this is a good paper. In general, I agree with Monniaux on all his points, except for his dislike of standard violating optimizations. We run our analytics on tens of thousands of processing nodes, so any optimization we can squeeze out is often worth the pain of fault finding and debugging. Online Computing Reviews Service

Access critical reviews of Computing literature here

Become a reviewer for Computing Reviews.

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Transactions on Programming Languages and Systems

ACM Transactions on Programming Languages and Systems Volume 30, Issue 3

May 2008

245 pages

ISSN:0164-0925

EISSN:1558-4593

DOI:10.1145/1353445

Issue’s Table of Contents

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 21 May 2008

Accepted: 01 June 2007

Revised: 01 April 2007

Received: 01 March 2006

Published in TOPLAS Volume 30, Issue 3

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

141
Total Citations
View Citations
2,833
Total Downloads

Downloads (Last 12 months)422
Downloads (Last 6 weeks)47

Reflects downloads up to 07 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

Kuhn LKlein BFröning H(2025)On the Non-associativity of Analog ComputationsMachine Learning and Principles and Practice of Knowledge Discovery in Databases10.1007/978-3-031-74643-7_15(183-195)Online publication date: 1-Jan-2025
https://doi.org/10.1007/978-3-031-74643-7_15
Chou YWu CJiang YKuo SKuo S(2024)Nanoscale Precision-Related Challenges in Classical and Quantum OptimizationIEEE Nanotechnology Magazine10.1109/MNANO.2024.337848818:3(31-43)Online publication date: Jun-2024
https://doi.org/10.1109/MNANO.2024.3378488
Konečný MPark SThies H(2024)Extracting efficient exact real number computation from proofs in constructive type theoryJournal of Logic and Computation10.1093/logcom/exae066Online publication date: 18-Oct-2024
https://doi.org/10.1093/logcom/exae066
Langer PAltmüller SFleisch EBarata F(2024)CLAIDFuture Generation Computer Systems10.1016/j.future.2024.05.026159:C(505-521)Online publication date: 1-Oct-2024
https://dl.acm.org/doi/10.1016/j.future.2024.05.026
Kneusel RKneusel R(2024)Floating PointNumbers and Computers10.1007/978-3-031-67482-2_3(79-113)Online publication date: 4-Dec-2024
https://doi.org/10.1007/978-3-031-67482-2_3
Misback EChan CSaiki BJun ETatlock ZPanchekha P(2023)Odyssey: An Interactive Workbench for Expert-Driven Floating-Point Expression RewritingProceedings of the 36th Annual ACM Symposium on User Interface Software and Technology10.1145/3586183.3606819(1-15)Online publication date: 29-Oct-2023
https://dl.acm.org/doi/10.1145/3586183.3606819
Garimella RSelva Balan MShukla VSampath S(2023)Role of artificial intelligence based image-processing techniques for port development activities in physical tidal modelsISH Journal of Hydraulic Engineering10.1080/09715010.2023.221410729:sup1(243-254)Online publication date: Jun-2023
https://doi.org/10.1080/09715010.2023.2214107
Martin-Dorel ÉMelquiond GRoux P(2023)Enabling Floating-Point Arithmetic in the Coq Proof AssistantJournal of Automated Reasoning10.1007/s10817-023-09679-x67:4Online publication date: 16-Sep-2023
https://dl.acm.org/doi/10.1007/s10817-023-09679-x
Sallinger SWeissenbacher GZuleger F(2023)A Formalization of Heisenbugs and Their CausesSoftware Engineering and Formal Methods10.1007/978-3-031-47115-5_16(282-300)Online publication date: 31-Oct-2023
https://doi.org/10.1007/978-3-031-47115-5_16
Le Mézo TJaulin LMassé DZerr B(2022)Kleene Algebra to Compute Invariant Sets of Dynamical SystemsAlgorithms10.3390/a1503009015:3(90)Online publication date: 8-Mar-2022
https://doi.org/10.3390/a15030090
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Cited By

Index Terms

Recommendations

The Floating-Point Unit of the Jaguar x86 Core

A Combined Interval and Floating Point Multiplier

Redundant-Digit Floating-Point Addition Scheme Based on a Stored Rounding Value

Reviews

Access critical reviews of Computing literature here