Satire: Computing Rigorous Bounds for Floating-Point Rounding Error in Mixed-Precision Loop-Free Programs

TL;DR

This work presents Satire, a tool for computing rigorous bounds on floating-point rounding errors in mixed-precision, loop-free programs that include conditionals. It combines backward-mode symbolic differentiation, path-strength reduction, and abstraction-guided optimization to achieve tight error bounds at scale, extending prior efforts to handle conditional branches and heterogeneous precision. The evaluation on large benchmarks, including Conjugate Gradient, demonstrates practical design-time value: mixed precision reduces error bounds without prohibitive runtime costs and enables informed trade-offs between accuracy and performance. These capabilities support robust numerical software design and verification in HPC contexts where precise error guarantees are critical.

Abstract

Techniques that rigorously bound the overall rounding error exhibited by a numerical program are of significant interest for communities developing numerical software. However, there are few available tools today that can be used to rigorously bound errors in programs that employ conditional statements (a basic need) as well as mixed-precision arithmetic (a direction of significant future interest) employing global optimization in error analysis. In this paper, we present a new tool that fills this void while also employing an abstraction-guided optimization approach to allow designers to trade error-bound tightness for gains in analysis time -- useful when searching for design alternatives. We first present the basic rigorous analysis framework of Satire and then show how to extend it to incorporate abstractions, conditionals, and mixed-precision arithmetic. We begin by describing Satire's design and its performance on a collection of benchmark examples. We then describe these aspects of Satire: (1) how the error-bound and tool execution time vary with the abstraction level; (2) the additional machinery to handle conditional expression branches, including defining the concepts of instability jumps and instability window widths and measuring these quantities; and (3) how the error changes when a mix of precision values are used. To showcase how \satire can add value during design, we start with a Conjugate Gradient solver and demonstrate how its step size and search direction are affected by different precision settings. Satire is freely available for evaluation, and can be used during the design of numerical routines to effect design tradeoffs guided by rigorous empirical error guarantees.

Figures (8)

• Figure 1: Error Analysis Workflow using Error Expression Optimization
• Figure 2: Reverse Mode AD
• Figure 3: Overview of Satire
• Figure 4: Path strength information for error propagating from y to s in an unrolled 3-point stencil evaluation across five time steps
• Figure 5: Abstractions introduced in a simple expression AST