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

FMiTF：Track-2：来自 LLVM 的严格且可扩展的形式浮​​点误差分析

• 批准号: 2319507
• 负责人: Ganesh Gopalakrishnan
• 金额: $ 10万
• 依托单位: University of Utah
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2023
• 资助国家: 美国
• 起止时间: 2023-08-01 至 2025-01-31
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2319507&HistoricalAwards=false
• 关键词: FMiTF; Track; Rigorous; Scalable; Formal; FMiTF; Track; Rigorous; Scalable; Formal

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.

该项目旨在通过确保由于有限的机器表示大小在可接受的限制范围内确保与不精确的错误相关的错误，以提高在现代处理硬件上运行的数值计算的可靠性。特别是，这项工作针对由浮点数系统系统引起的算术舍入。鉴于关键的科学模拟数据或重要的机器学习相关数据在计算机内存中表示，要包含数值错误很重要。随着为了减少能源消耗而越来越多地对数据移动进行优化的压力，许多程序正在转向较低的精度数值表示。这种趋势可能会引入其他错误，因此，人们真的不能希望消除所有错误，而是设计可容忍此错误的算法。该项目基于多功能和流行的LLVM语言技术开发一个框架，可以在其中插入多个协作错误分析工具。这项工作中采用的核心技术方法是LLVM作为错误分析的常见中间形式的选择。尽管已经创建了许多用于此类错误分析的学术研究工具，但它们不能互操作，也不能允许传统程序受到错误分析。该项目提出了一个称为llfperror的框架，该框架允许集成不同的错误类型的错误分析工具。这为设计师提供了数值错误的全面图片，包括突出显示诸如灾难性取消，浮点异常和浮点圆形错误等错误。错误分析工具的研究和完善必须由现实的编程结构驱动，但以简化的形式提供，以免淹没分析工具。在这方面，llfperror将在现场使用的现实内核上运行程序切割工具。这样，llfperror将不会冒着分析范围内范围内的示例的风险。 这还允许该项目硬化现有的错误分析工具，并开发新的工具，并释放此类工具以及我们的扩展基准套件。在两年中，该项目将释放集成错误分析工具以及现实的示例。这有助于满足高性能计算（HPC）和机器学习（ML）的重要需求之一，即通用和全面的错误分析。我们的最终目标是帮助建立针对HPC和ML的工具建设者的社区，从而为更可靠的科学模拟以及可靠且可解释的机器学习铺平道路。该奖项反映了NSF的法定任务，并被认为是值得通过基金会的知识分子和更广泛影响的评估来通过评估来获得支持的。