FPBench at FM’18
Combining Tools for Optimization and Analysis of Floating-Point Computations
Combining Tools for Optimization and Analysis of Floating-Point Computations
The second paper on FPBench was published at the Formal Methods conference in 2018.
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.
The paper uses the FPBench benchmarks and tooling to combine and compare the Herbie and Diasy tools. The paper demonstrates the importance of testing combinations of tools and describes some of the challenges that had to be surmounted. It is available in PDF format. All code described in the paper is also freely available online.