浮点计算优化与分析的组合工具
Combining Tools for Optimization and Analysis of Floating-Point Computations
摘要：
最近，对优化和分析浮点程序的兴趣重新燃起，导致了一系列用于数值程序的新工具。这些工具通常是互补的，每一个都专注于数值编程的一个不同方面。构建可靠的浮点应用程序通常需要解决其中的几个方面，这使得简单的组合变得至关重要。本文介绍了两个最近的浮点工具的组成：Herbie，它执行精度优化，和Daisy，它执行精度验证。我们发现，这种组合为用户提供了许多好处，例如能够使用Daisy来检查Herbie的不合理优化是否改善了最坏情况下的舍入误差，以及对工具作者的好处，包括发现两个工具中的一些错误。这种结合也使我们能够第一次比较这些工具实现的不同程序重写技术。本文为结合其他浮点工具和克服常见挑战提供了路线图。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
