A Verification Toolchain for the Round-Off Error Analysis of Multiprecision Floating-Point Programs
Ariel Kellison, Cornell University
Pipelined and multiprecision versions of core numerical algorithms play a central role in adapting scientific computing software stacks to modern heterogeneous HPC systems. Analyzing the accuracy and stability of pipelined and multiprecision numerical algorithms, particularly in the presence of overflow and underflow, presents a significant challenge. Furthermore, a gap exists between the guarantees provided by traditional error analysis of an algorithm and the behavior of a particular implementation of that algorithm: is unexpected behavior due to a bug in the implementation or approximations that were made in the error analysis? We are pursuing the development of a toolchain that can connect guarantees of numerical accuracy and stability of an algorithm and its pipelined or multiprecision variations to guarantees of the correctness of a particular imperative implementation; these guarantees are made only under the assumptions of the IEEE-754 specification of floating point arithmetic and the operational semantics of the underlying imperative programming language. This poster will focus on our recent advances toward developing a verification tool that unifies and semi-automates multiprecision round-off error analysis for numerical algorithms. Significantly, our analysis toolchain captures the possibility of underflow and overflow, and provides machine-checkable proof certificates as evidence for our guarantees of accuracy and program correctness. This is joint work with Andrew Appel (Princeton University), David Bindel (Cornell University), Geoffrey Hulette (Sandia National Laboratories, CA), and Heidi Thornquist (Sandia National Laboratories, NM).
Abstract Author(s): Ariel Kellison