PaperlayerView exact revision on arXiv

Source-linked AI summary

The pitfalls of verifying floating-point computations

David Monniaux

arXiv:cs/0701192v5cs.PLmath.NA

TL;DR

Critical systems increasingly depend on floating-point, but its effective semantics can vary with hardware, compilers, libraries, and runtime context, complicating testing and verification. The paper gives concrete failure cases and presents sound-analysis adaptations, showing both serious reproducibility hazards and practical ways to reason about them.

  • Problem

    Floating-point implementations can vary beyond source-code semantics, creating difficulties for testing and static analysis of critical applications.

  • Method

    The paper examines implementation, rounding, I/O, and language-level pitfalls and explains sound verification and abstract-interpretation techniques that account for concrete floating-point semantics.

  • Results

    The same expression can yield different results on Intel 32-bit systems when seemingly irrelevant statements alter temporary-register handling.

  • Takeaways & Limitations

    Sound floating-point analysis is feasible for some application classes, although verification proofs may become more complex because of increased nondeterminism.

  • Takeaways & Limitations

    The discussed reproducibility problem is especially associated with Intel 32-bit temporary handling, and proposed sound proof alterations increase nondeterminism and proof complexity.

Abstract

from arXiv · show

Current critical systems commonly 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 with many factors beyond source-code level, such as choices made by compilers. We here give concrete examples of problems that can appear and solutions to implement in analysis software.

1 Introduction

Floating-point semantics in critical applications depend on implementation and software context, complicating testing, validation, and program analysis. The paper catalogs these pitfalls and explains how sound analysis can still be achieved.

  • Motivation: Critical applications increasingly use floating-point operations and therefore require stringent testing or validation.The paper focuses on automotive and aerospace control applications as examples.
  • Implementation dependence: IEEE compliance does not uniquely determine program behavior because compiler, library, runtime, and hardware interactions affect the application-level environment.The paper emphasizes that compatibility must be assessed as experienced by the programmer or system user.
  • Implementation dependence: On Intel platforms, 80-bit internal registers, register allocation, and logging instructions can change final results without apparent changes to the computation.These effects can invalidate assumptions that repeated expressions remain stable when their source variables are unchanged.
  • Consequences: Floating-point oddities can produce rare, extremely hard-to-diagnose runtime errors in seemingly innocuous industrial code.The paper presents a complete real-life code example to illustrate this failure mode.
  • Sound analysis: Sound floating-point analysis is feasible when analyses account for concrete floating-point semantics and associated error bounds.Astrée is presented as a mathematically sound analyzer used in an industrial context with reasonable cost for some application classes.

2 IEEE-754: a reminder

IEEE-754 defines floating-point representations, special values, exceptions, and rounding modes, but their computational consequences require careful treatment. Bounded exponents, underflow, conversion, and repeated rounding create important error and reproducibility issues.

  • Representations: IEEE-754 implementations commonly support normal, subnormal, infinite, NaN, and signed-zero values.Subnormal values are close to zero and pose special rounding-error issues; signed zeros can affect operations such as division.
  • Exceptions: IEEE exceptions include invalid operation, overflow, division by zero, underflow, and inexact results.Silent responses include NaN, infinities, or rounded values, and sound analysis must account for these behaviors.
  • Representations: Floating-point values use a signed significand and exponent, with precision and exponent bounds determining representable values and ulp size.For a normalized representation, x = ±s.m with s = 2^e and ε_last = 2^-(p−1).
  • Rounding: Rounding modes map real values to floating-point values differently, including directed rounding toward +∞, −∞, zero, and nearest.Round-to-nearest is the default mode and is used by the vast majority of programs.
  • Error and reproducibility: Bounded exponent ranges invalidate purely relative error bounds because overflow and least-positive values introduce absolute error near zero.Decimal conversion and library I/O can also introduce inaccuracies, undermining exact replay of test cases.

3 Architecture-dependent issues

Floating-point results can change with register allocation, compiler optimisations, function inlining, logging, and repeated rounding, even when source-level computations appear unchanged. These architecture- and compilation-dependent effects complicate testing and semantic analysis.

  • x87 register behavior: Register allocation changes whether intermediate values remain in extended-precision x87 registers or are spilled to memory and rounded.Compilers spill extra temporaries when registers are insufficient, while optimised code may keep program variables in x87 registers.
  • Optimisation and overflow: 10308 versus +∞ demonstrates that compilation options can change results when extended-precision computations avoid an intermediate double-precision overflow.Optimised code reuses a register-held value, whereas non-optimised code saves and reloads it through memory.
  • Inlining: Inlining changes whether a value is converted to double precision during parameter passing, producing 10308 with optimisation and +∞ without it.Without inlining, the square result is returned in long double format but passed as a double; with inlining, no such conversion occurs before division.
  • Comparisons and spills: Strict comparisons can disagree because a value tested in extended precision may later be rounded to zero or another single- or double-precision value.The outcome depends on optimisation, separate compilation, and seemingly inert calls such as do_nothing().
  • Debugging effects: Logging and debugging can alter computational results by changing register scheduling, causing spills, reloads, and additional rounding.Disabling optimisation for debugging can also change results, despite leaving the source computation unchanged.
  • Double rounding: Double rounding can differ from direct rounding in round-to-nearest mode, including cases where one result remains finite while another becomes +∞.The effect arises when values are first rounded in extended precision and then rounded again for double-precision storage; underflow can similarly produce differing subnormal results.

4 Mathematical functions

Floating-point behavior depends not only on IEEE-754 arithmetic but also on libraries, processors, compilers, rounding modes, and input/output conventions. These dependencies can produce discrepancies that undermine testing and static analysis.

  • Mathematical libraries: IEEE-754 specifies elementary operations but not popular functions such as sine and cosine, which are supplied by libraries or hardware.Their behavior can vary across libraries, processor manufacturers, and processor models.
  • Mathematical libraries: 11.5% error occurred for GNU libc’s sin(p) result compared with Pentium 4 x87 and Mathematica for a carefully chosen large input.The example exposes imprecision in reduction modulo 2π when the true sine is close to zero.
  • Mathematical libraries: 3–4.5 ulps were reported as typical worst-case transcendental-function errors on the Intel486 with Intel 387 coprocessor.The error was sometimes as large as 4.5 ulps.
  • Compilers: Compilers may apply disallowed associativity and special-value optimisations, so source-level analysis may not describe the generated object code.On SSE, some compilers compile four real-number-equivalent min/max expressions identically despite differences involving NaNs and signed zeros.
  • Input/output: Decimal floating-point input and output are difficult to make exact, so hexadecimal constants and %a/%A formats are suggested where compiler and library support permits.Exact printing and reading matter for replaying test cases.

5 Example

A realistic modulo-and-table-lookup example shows that seemingly equivalent floating-point code can behave differently across compilation conditions and crash for rare inputs. Static analysis and targeted testing can expose failures that random testing misses.

  • Overview: A modulo algorithm correct over real numbers, combined with tabulated-function implementations, can crash for specific inputs on certain platforms.The composed implementation maps angles into [−180, 180] before performing table lookups.
  • Modulo computation: Optimised x87 compilation returned r ≃179.99999999999997158, whereas non-optimised compilation returned r ≃−180.00000000000002842 outside the specified bounds.Register-resident extended precision versus memory-spilled double precision caused the difference.
  • Modulo computation: Logging can reproduce the non-optimised result because function calls force floating-point registers to spill into memory.Rewriting the code so the compiler holds the value in a register makes the problem disappear.
  • Testing implications: Astrée rejected the modulo code’s post-condition, while ordinary unit testing on an IA32 PC missed the bug without carefully chosen values near discontinuities.The failure was found by searching for counter-examples after the static analyser produced a slightly out-of-bounds interval.
  • Table lookup: A table lookup just below −180 may access table[-1], yielding a segmentation fault, NaN, infinity, or an unexpectedly large value.With table[-1] = 10^308 and table[0] = 0, the interpolated output was approximately 2.8 × 10^294.
  • Testing implications: Rare floating-point failures are difficult to reproduce, unlikely under random testing, and may disappear under another compiler, option, or execution platform.Mass-produced systems can make individually rare inputs operationally significant.

6 A few remarks on Java

Java’s intended floating-point predictability is undermined by x87 excess precision, compiler behavior, and JIT execution choices. The examples show that compilation mode and runtime system can change results even for the same program.

  • Java semantics: Java’s early floating-point model aimed at strict IEEE-754 single- and double-precision arithmetic, but strict compatibility is difficult on x87.The discussion examines compiler and runtime consequences of that difficulty.
  • Implications: These effects introduce platform dependencies that conflict with Java’s intended unique semantics for single-threaded programs without system-dependent features.The conclusion recommends caution when assuming predictable floating-point behavior.
  • Compiler behavior: The same Java computation printed Infinity without optimisation, 1E308 at -O, and Infinity at -O3 on an x87 target.Intermediate spilling, register retention, and constant folding produced the different outputs.
  • Compiler behavior: gcj ignored strictfp, despite strictfp being intended to force strict IEEE-754 round-to-nearest semantics.The author also questions whether the observed behavior is correct under the language specification.
  • Runtime behavior: Interpreted, JIT-compiled, and JIT-specialised execution may produce three different floating-point results for one function.JIT compilation can dynamically change semantics for reasons unrelated to the program’s inputs.

7 Implications for program verification

Formal verification has historically ignored floating-point computations because their semantics were considered too difficult to model. This motivates verification techniques that explicitly account for floating-point behavior.

  • Verification gap: Formal methods have long ignored floating-point computations because they were judged too baroque or difficult to model.The section frames floating-point semantics as a challenge for proving programs fit their specifications.

7.1 Goals of program verifications

Program verification for floating-point code ranges from preventing runtime failures to bounding numerical error and proving conformance to a numerical specification. These goals become progressively more demanding as they move from safety properties toward semantic accuracy.

  • Safety and error goals: Verification may first target the absence of undefined or undesirable behaviors, including overflow during floating-point-to-integer conversion.The Ariane 5 failure was attributed to overflow converting a 64-bit floating-point value to a 16-bit integer.
  • Safety and error goals: Bounding overflow requires finding bounds for values, which can require proving stability when computations depend on prior inputs and outputs.The paper cites infinite impulse response filters, rate limiters, and combinations as examples.
  • Analysis tools: Astrée bounds variables and attempts to prove the absence of overflows and other runtime errors, but it is not designed to prove arbitrary user-defined properties.Users can specify assertions such as bounds on variables representing physical quantities, which Astrée attempts to prove.
  • Safety and error goals: Roundoff analysis identifies where numerical errors originate and proves upper bounds on their magnitude in program variables.The Fluctuat tool is presented as automatically providing such results.
  • Safety and error goals: The strongest goal is proving that a program implements a specified numerical computation within a specified error bound.Except in simple cases, automated methods are unsuitable, while computerised proof assistants may help with formal proofs.

7.2 Semantic bases of program analysis

Sound verification requires a semantics that models all concrete program behaviors, but simplifying semantics can make analysis tractable only when it does not remove possible behaviors. Treating floating-point values as reals may therefore suit bug finding but is risky for sound assurance.

  • Soundness and abstraction: A mathematical program semantics for sound proofs should model all possible concrete system behaviors without omission.This semantics provides the mathematical characterization of what a program actually does.
  • Soundness and abstraction: A semantics that omits concrete behaviors can make verification simpler, but it is risky when the goal is assurance that the program performs correctly.The paper reports that simple programs correct over reals can exhibit odd or fatal floating-point behavior.
  • Soundness and abstraction: Real-number semantics may be suitable for unsound bug-finding systems, which trade soundness for fewer false warnings and faster analysis.Such systems aim to direct programmers toward probable bugs rather than prove their absence.
  • Soundness and abstraction: Sound analysis can be undermined by starting from a floating-point semantics that does not accurately model reality.The paper frames this as an easy way for an analysis designer to build an unsound static-analysis tool unintentionally.
  • Soundness and abstraction: Because terminating automatic analyses are incomplete, they may safely simplify by adding behaviors rather than removing behaviors from the concrete system.The paper presents this as a way to preserve soundness while making analysis more tractable.

7.3 Difficulties in defining sound semantics

Defining sound floating-point semantics from source code is difficult because implementation behavior depends on processors, compilers, libraries, and runtime choices. The paper presents exact machine-level semantics and nondeterministic abstractions as alternatives to naive source-level modeling.

  • Semantic approaches: Sound semantics must characterize what floating-point programs actually do, but source-level definitions face multiple implementation-dependent behaviors.The paper introduces several approaches for handling these difficulties.
  • Semantic approaches: Naively mapping source-level float and double operators to strict IEEE-754 operations fails in many common cases, especially on x87.The naive model assumes each operation rounds directly to the target precision.
  • Semantic approaches: Analyzing assembly or object code can use exact processor-specified operation semantics and is likely preferable when compiler optimizations are not trusted.Source-level information can still assist assembly analysis through invariant translation.
  • Semantic approaches: Advanced floating-point functions may differ across processor generations, although knowing the target processor can provide behavior information for embedded-system analysis.The paper also suggests avoiding poorly specified processor functions.
  • Semantic approaches: Abstract interpretation can remain sound by encompassing all possible source-code semantics, including implementation-defined behaviors.This approach is presented as a third alternative to naive source semantics and direct machine-code analysis.

7.4 Hoare logic

Straightforward Hoare logic is unsound when floating-point expressions lack a unique meaning, as on x87 or fused-multiply-add architectures. Soundness can be recovered through assembly-level reasoning or nondeterministic semantics, but these workarounds are costly and depend on compiler knowledge.

  • Hoare logic foundations: Hoare logic reasons from hypotheses H1 ... Hn to a conclusion C by applying a rule, with zero hypotheses forming an axiom.The rules cover assignments, sequences, and tests and rely on an underlying mathematical logic.
  • Hoare logic foundations: Floating-point Hoare rules require expressions to retain their floating-point meaning and distinguish operators by precision when multiple types are used.A proof assistant must reason about rounded floating-point quantities, such as x ⊕ y defined through an appropriate rounding function.
  • Sources of unsoundness: Standard Hoare rules become unsound when arithmetic expressions can change value without source variables changing, as on architectures such as x87.They are sound only when rounding points are precisely known.
  • Sources of unsoundness: The x87 architecture has rounding points affected by register scheduling, while fused multiply-add permits either separately rounded or fused evaluation.For x ⊗ y ⊕ z, the alternatives are r(r(x × y) + z) and r(xy + z).
  • Soundness workarounds: Analyzing generated assembly provides unambiguous semantics, but directly checking assembly is strenuous because it exposes low-level concerns hidden by high-level languages.The approach applies at least to basic arithmetic and square-root operations; transcendental functions may be less specified.
  • Soundness workarounds: Nondeterministic rounding semantics decomposes compound assignments and permits rounding at possible implementation points, covering all compilation choices represented by the model.The transformed code can then be handled by Hoare logic, and additional compiler or ABI knowledge can reduce nondeterminism.
  • Soundness workarounds: Fused multiply-add can be handled by nondeterministically choosing between separately rounded and fused real-arithmetic expressions.This technique depends on knowing how the compiler may group expressions, and that set may be large because optimizations cross instructions and function calls.
  • Conclusion: Hoare-logic provers are hampered by platforms or languages without a single expression meaning; straightforward rules may be unsound, and workarounds are possible but costly.The paper states this as a summary of its findings.

7.5 Static analysers based on abstract interpretation

Sound abstract interpretation of floating-point programs requires modeling implementation-specific execution before applying ideal abstract domains. These abstractions can remain sound, but implementation details such as extended precision, double rounding, and hidden rounding operations must be reflected.

  • Abstraction framework: Abstract interpretation over-approximates possible program executions using symbolic constraints such as intervals and octagons.Its abstraction pipeline moves from floating-point semantics to nondeterministic real semantics, then to an ideal abstract domain and, optionally, an effective implementation.
  • Intervals: Interval analysis attaches each program quantity an interval containing its value in every concrete execution.Efficient computation requires matching the analyzer’s arithmetic types and rounding behavior to the concrete IEEE-754 system.
  • Intervals: Naively combining interval endpoints is unsound when extended-precision temporaries or double rounding affect program computations.This is particularly relevant on x87 platforms, where register spills can change effective precision.
  • Intervals: Strict-comparison bounds must account for the exact precision used by comparisons and for later rounding to lower precisions.Using pred at the extended precision and then rounding bounds may reduce the abstraction to one equivalent to treating < like ≤; exact representability can permit tighter bounds.
  • Numerical relational domains: Relational domains must bridge ideal arithmetic structures and concrete floating-point execution, including adjusted error bounds for possible double rounding.The paper gives |x − r(x)| ≤ εrel.|x| + εabs as an error model and notes that εrel must compensate for double rounding.
  • Soundness: The analysis is sound because it ignores no program behavior, but incomplete because abstraction introduces behaviors that cannot occur concretely.If floating-point semantics are modeled unsoundly in the first abstraction step, the whole analysis can become unsound.
  • Numerical relational domains: Propagated arithmetic identities may fail when hidden rounding operations or modes such as flush-to-zero affect execution.Consequently, relations such as x ⊖ y = 0 ⇔ x = y cannot always be treated as valid.

7.6 Testing

Testing floating-point software on a development platform can be risky because target behavior may differ across IEEE-754-compatible systems or depend on compilation details. Sound replay-based analysis likewise requires an exact semantic model of execution on the target platform.

  • Platform differences: Development and target platforms may differ in speed and availability, encouraging testing on the development platform.For embedded systems, the target is often a slower microcontroller with limited availability for the development group.
  • Platform differences: IEEE-754 compatibility does not guarantee identical behavior across development and target platforms.The paper characterizes substituting the development platform for the target as risky even when both claim IEEE-754 compatibility.
  • Compilation effects: On x87 systems, register scheduling can change results, and inserting monitoring instructions can alter register allocation and final computation.Setting 53-bit mantissa precision can limit, but not completely eliminate, discrepancies when using only IEEE-754 double precision numbers.
  • Replay-based analysis: Static-analysis techniques that replay concrete traces require an exact semantic model of the program as it runs on the target platform.The same platform-specific execution concerns therefore apply to replay-based analysis, not only to unit testing and debugging.

8 Conclusion

Common floating-point platforms can produce different results despite standards conformance, complicating testing, debugging, and verification. The paper proposes sound adaptations for verification and analysis while emphasizing reproducibility and conscious treatment of unsafe compiler optimizations.

  • Reproducibility: Subtle floating-point differences across common software and hardware platforms create problems for unit testing and debugging unless the exact target object code is used.Standards conformance alone does not ensure identical floating-point behavior.
  • Reproducibility: On some platforms, the same expression can yield different results with unchanged variables and compiler when seemingly irrelevant statements alter temporary-variable handling.On Intel 32-bit systems, a condition can hold and then cease to hold two source lines later without an intervening source-level modification.
  • Analysis and verification: The paper modifies Hoare-logic verification techniques for systems where repeated evaluation is not stable and gives sound abstract-interpretation techniques for Intel 32-bit platforms.The abstract-interpretation approach includes precise handling of strict comparisons.
  • Design implications: Reproducibility is presented as paramount for safety-critical applications because result changes from seemingly irrelevant circumstances complicate debugging and can make analyses unsound.The paper specifically highlights compilation schemes in which inserting a print statement can change results.
  • Design implications: Compiler optimizations that contradict published language standards or break verification techniques may improve performance, but their use should be conscious.The concern is framed as a design and configuration issue for compilers and systems.
Loading cs/0701192v5…