SHF: Small: Formalisms, Implementations, and Verification Procedures for Alternatives to Floating Point

Efficient and accurate representation of real numbers is a foundational question in computer science. A floating-point number is widely used to approximate a real number using a finite number of bits. Given the need for good performance and challenges in reasoning about rounding errors or exceptional conditions with the floating-point representation, there is interest in the community to explore possible alternatives to it. The Posit representation is a recently proposed alternative to the IEEE-754 floating point representation. This project develops techniques, tools, and procedures to determine whether Posit is a viable alternative to floating point. This project's impacts are the following: (1) enable programmers to effectively write correct programs using Posits, (2) make foundational advances for generating high-performance math libraries and automated reasoning for Posits, (3) influence domain experts in scientific computing and alleviate their concerns about correctness and accuracy, and (4) educate graduate, undergraduate, and high-school students on foundational abstractions and reasoning techniques. The Posit representation can represent more real numbers than the floating-point representation given the same number of bits. Depending on the configuration, it can represent every real value that floating point can. The Posit community is attempting to find specific applications where a Posit outperforms floating point in accuracy, performance, or storage. This project develops techniques, tools, and procedures to reason about the feasibility, performance, and accuracy of applications written with Posits. Specifically for performance, the project develops high performance math libraries for the Posit representation and explores hardware support for Posit operations. To reason about the accuracy of computation, the investigators develop techniques for fast shadow execution that compares a Posit execution to an execution with real numbers. To enable automated reasoning for programs using Posits, the project develops a theory of Posits usable with satisfiability modulo theory solvers. 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.