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.