Collaborative Research: CS2: Deriving Correct Programs for Performant Computational Chemistry

Many scientific fields rely on high-performance computing in order to accurately simulate complex physical phenomena involving high dimensional tensors (multi-dimensional arrays). In particular, implementations of algorithms in the domain of computational quantum chemistry follow one of two paths: excruciatingly slow and error-prone expert hand-coding which results in very fast but inflexible code, or general, library-based (or code generation-based) development, which reduces development effort but often leaves significant performance on the table. The project's impact is to enable provably correct (correct by construction) code generation of key computational routines in a high-performance manner that can be incorporated into larger code bases. This contributes to the overall goal of whole-program verification of scientific applications. The project’s novelties are 1) new notations for describing operations involving structured matrices and tensors, 2) new insights to identify high-performance algorithms from their specification, and 3) integrating complex data movement into the specification of the algorithm to better identify and exploit optimization opportunities at various abstraction levels. Techniques and algorithms developed by the project will broadly impact the theory and practice of computational science, data science, and machine learning. All aspects of the work will involve the training of young scientists at the graduate and undergraduate student levels. This project leverages and extends the Formal Linear Algebra Methods Environment (FLAME), a proven methodology for the correct-by-construction development of dense linear algebra algorithms, to structured tensors and novel high-level linear algebra operations which commonly arise in computational chemistry. Real-world examples of linear algebra and tensor operations in computational chemistry applications will be used to develop new notations and abstraction levels. Desirable performance characteristics will be captured using the developed notations in the specification and at the loop invariant level to identify and derive high performance algorithms. The performance of the resulting implementations will be benchmarked against those in standard packages. 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.