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

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.