FMiTF: Track-2 : Rigorous and Scalable Formal Floating-Point Error Analysis from LLVM

该项目旨在通过确保有限的机器表示大小引起的不精确相关误差在可接受的范围内来提高在现代处理硬件上运行的数值计算的可靠性。特别是，这项工作的目标是浮点数系统引起的算术舍入。考虑到关键的科学模拟数据或与机器学习相关的重要数据都在计算机内存中表示，控制数值误差是很重要的。随着优化数据移动以降低能耗的压力越来越大，许多程序正在转向更低精度的数值表示法。这种趋势可能会引入额外的错误，因此人们不能真的希望消除所有错误，而是设计出容忍这种错误的算法。该项目基于通用和流行的LLVM语言技术开发了一个框架，在该框架中可以插入多个协作的错误分析工具，其核心技术方法是选择LLVM作为错误分析的通用中间形式。虽然已经创建了许多用于这种错误分析的学术研究工具，但它们不能互操作，也不允许传统程序受到错误分析的影响。该项目提出了一个名为LLFPError的框架，它允许集成针对不同错误类型的错误分析工具。这为设计者提供了一个全面的数值误差图景，包括突出显示灾难性抵消、浮点异常和浮点舍入误差等误差。错误分析工具的研究和改进必须由现实的编程构造驱动，但要以简化的形式提供，以免淹没分析工具。在这方面，LLFPError将在该领域中使用的真实内核上运行程序切片工具。有了这一点，LLFPError将不会有分析范围狭窄的示例的风险。这也允许该项目加强现有的错误分析工具，以及开发更新的工具，并将这些工具与我们扩展的基准测试套件一起发布。该项目历时两年，将发布综合误差分析工具和实际例子。这有助于满足高性能计算(HPC)和机器学习(ML)中的一个重要需求，即通用和全面的误差分析。我们的最终目标是帮助发展面向HPC和ML的工具制造商社区，从而为更可靠的科学模拟以及可靠和可解释的机器学习铺平道路。该奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

This project aims to enhance the reliability of numerical computations running on modern processing hardware by ensuring that the imprecision related errors due to finite machine representation sizes are within acceptable limits. In particular, this work targets arithmetic rounding caused by the floating-point number system. It is important to contain numerical error, given that critical scientific simulation data or important machine learning-related data are represented inside the computer memory. With the growing pressure to optimize on data movement in order to reduce energy consumption, many programs are switching to even lower precision numerical representations. This trend can introduce additional errors and hence one cannot really hope to eliminate all the error, but instead design algorithms that tolerate this error. This project develops a framework based on the versatile and popular LLVM language technologies within which multiple collaborating error analysis tools can be plugged in.The core technical approach taken in this work is the choice of LLVM as a common intermediate form for error analysis. While many academic research tools for such error analysis have been created, they cannot interoperate nor allow traditional programs to be subject to error analysis. The project proposes a framework called LLFPError that allows error analysis tools that target different error types to be integrated. This provides the designer with a comprehensive picture of numerical errors, including highlighting errors such as catastrophic cancellation, floating-point exceptions and floating-point rounding errors. The study and refinement of error analysis tools must be driven by realistic programming constructs but offered in a simplified form so as not to inundate the analysis tool. In this regard, the LLFPError will run program-slicing tools on realistic kernels that have been employed in the field. With this, LLFPError will not run the risk of analyzing examples that fall within a narrow scope. This also allows this project to harden existing error analysis tools as well as develop newer tools and release such tools along with our extended benchmark suite. This project, across two years, will result in the release of integrated error analysis tools as well as realistic examples. This helps meet one of the important needs in high performance computing (HPC) and machine learning (ML), namely versatile and comprehensive error analysis. Our eventual goal is to help grow the community of tool builders who target HPC and ML, thus paving the way for more reliable scientific simulations as well as reliable and explainable machine learning.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.