Collaborative Research: CS2: A Comprehensive Pipeline for Formal Verification of Floating-Point Errors and Compilation for Scientific Computing

Regents Of The University Of Michigan - Ann Arbor, Ann Arbor MI

Investigators

Abstract

Scientific computing (SC) involves using advanced computing capabilities to understand and solve complex physical problems. With the increasing complexity of physical models and a rise in demand for high-performance computing (HPC) resources, errors can occur at all levels of abstraction in the computing process, significantly impacting the process of computer driven-scientific discovery and decision-making. Thus, correctness in scientific computing remains a formidable challenge. Prior works have attempted to verify a numerical program end-to-end but fall short in terms of scalability in the proof process, and target an idealized implementation of a numerical program. This project addresses this gap by developing a scalable verification framework, which directly targets application SC libraries written in Low Level Virtual Machine (LLVM)-compatible programming languages, like C/C++, Fortran and Julia, instead of an idealized implementation. The project's novelties are mechanized functional models for SC algorithms, accuracy and stability proofs of critical numerical algorithms in reduced- and mixed-precision floating-point (FP) formats, and the development of evidence and assurance cases for guaranteed correctness of future ports to new accelerated hardware. The project's impacts are an increased productivity of model developers, by providing a framework for root cause analysis of numerical bugs, and strong assurance cases for highly performant SC applications. This project addresses the fundamental challenges of creating a scalable end-to-end verification of SC code by addressing issues in each of the following abstraction layers: (1) numerical behavior at the compiler level by rigorously modeling compiler optimizations for FP arithmetic and extending the translation validation framework of the Crellvm tool (which performs Coq-verified translation validation for LLVM), to prove correctness of FP optimizations at the compiler intermediate representation level; (2) modeling approximations in mathematical formulations by mechanizing the FP error model for reduced- and mixed-precision analysis, and formalizing the correctness properties of chosen SC modules, like the convergence and stability of numerical algorithms, with respect to the mechanized error model; and (3) algorithmic approximations in various HPC libraries by verifying that the HPC libraries implement the mathematics correctly by connecting the mechanized proofs of mathematical correctness to the compiler FP optimization correctness proof. The investigators also propose to develop several automations to boost scalability and productivity of end-to-end verification of SC applications. These methods will be applied in the context of matrix-free finite element algorithms in problems related to inertial confinement fusion and plasma applications. To increase adoption of formal tools in the scientific computing communities, key ideas and theories in formal methods will be disseminated through workshops and seminar series, thereby bringing together two widely separate communities, formal methods and scientific computing. 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.