FMiTF: Track II: Rigorous and Versatile Float-Point Precision Analysis and Tuning

University Of Utah, Salt Lake City UT

Investigators

Abstract

Floating-point numbers serve as the mostly commonly used representation within computers of real-valued quantities such as the average global temperature on Earth. Since computer storage cells have finite precision, floating-point quantities must be suitably rounded, following standard rounding rules such as promulgated by the Institute of Electrical and Electronics Engineers (IEEE). Unfortunately, these rounding rules are sometimes incorrectly implemented in existing pieces of important software. In other cases, key links in the software transformation pipeline deviate from mathematical stipulations. This project provides an integrated collection of tools called FPFormal that helps establish mathematically rigorous estimates of round-off error. It assists designers pinpoint exactly which links in the transformation pipeline must be enhanced to attain certifiable calculation results. This research eliminates or vastly minimize deviations in calculation results that inform critical scientific decisions. The tools developed in this project will be open to the entire scientific community, and also play a key role in promoting pedagogy at all levels of computing education. The FPFormal project provides an integrated collection of point tools that help researchers in science and engineering establish tight round-off error bounds for their numerical calculations. Some of these tools employ symbolic differentiation supported by a novel idea called Taylor Forms, feeding the results to a global optimizer called Gelpia. Other tools in FPFormal will help pinpoint the sources of result deviations through differently branching computations. They will also compute inputs that cause the most roundoff errors. FPFormal will be released to the research community and promoted at conferences and workshops specifically targeting three groups: computational scientists at national laboratories; companies invested in developing mathematical software; and individual researchers in areas such as Physics where calculations are the only means of exploring the unknown. A major emphasis of the investigators will be to adhere to standards such as FPBench being developed by the community to supply well-vetted benchmarks. Broader impacts of the project are to equip domain science and engineering researchers and practitioners with tools that help them make their computational software trustworthy as well as more energy efficient, by enabling them to choose lower precision whenever the underlying specifications allow. Potential impacts span both high-performance computing and 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.