Automatic Verification of Floating-Point Accumulation Networks

TL;DR

This paper introduces an automatic verification method for floating-point accumulation networks, providing rigorous correctness proofs and tight error bounds, along with a new, faster, and more accurate FPAN for double-double addition.

Contribution

It presents a novel automated verification approach for FPANs, including a new, improved FPAN algorithm for double-double addition.

Findings

Verified correctness properties with tight error bounds

Developed a faster, more accurate FPAN for double-double addition

Introduced a new floating-point abstraction model

Abstract

Floating-point accumulation networks (FPANs) are key building blocks used in many floating-point algorithms, including compensated summation and double-double arithmetic. FPANs are notoriously difficult to analyze, and algorithms using FPANs are often published without rigorous correctness proofs. In fact, on at least one occasion, a published error bound for a widely used FPAN was later found to be incorrect. In this paper, we present an automatic procedure that produces computer-verified proofs of several FPAN correctness properties, including error bounds that are tight to the nearest bit. Our approach is underpinned by a novel floating-point abstraction that models the sign, exponent, and number of leading and trailing zeros and ones in the mantissa of each number flowing through an FPAN. We also present a new FPAN for double-double addition that is faster and more accurate than the previous best known algorithm.