Combining Tools for Optimization and Analysis of Floating-Point Computations

TL;DR

This paper explores combining two floating-point tools, Herbie and Daisy, to improve accuracy optimization and verification, revealing benefits, uncovering bugs, and enabling new comparisons in numerical program analysis.

Contribution

It demonstrates the first successful integration of accuracy optimization and verification tools for floating-point programs, enhancing reliability and revealing new insights.

Findings

Daisy can verify Herbie's optimizations for worst-case error.

The combination uncovers bugs in both tools.

It enables comparison of different rewriting techniques.

Abstract

Recent renewed interest in optimizing and analyzing floating-point programs has lead to a diverse array of new tools for numerical programs. These tools are often complementary, each focusing on a distinct aspect of numerical programming. Building reliable floating point applications typically requires addressing several of these aspects, which makes easy composition essential. This paper describes the composition of two recent floating-point tools: Herbie, which performs accuracy optimization, and Daisy, which performs accuracy verification. We find that the combination provides numerous benefits to users, such as being able to use Daisy to check whether Herbie's unsound optimizations improved the worst-case roundoff error, as well as benefits to tool authors, including uncovering a number of bugs in both tools. The combination also allowed us to compare the different program rewriting techniques implemented by these tools for the first time. The paper lays out a road map for combining other floating-point tools and for surmounting common challenges.