权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

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

SHF：小：浮点替代方案的形式主义、实现和验证程序

基本信息

批准号：
1908798
负责人：
Santosh Nagarakatte
金额：
$ 50万
依托单位：
Rutgers University New Brunswick
依托单位国家：
美国
项目类别：
Standard Grant
财政年份：
2019
资助国家：
美国
起止时间：
2019-07-01 至 2024-12-31
项目状态：
已结题

来源：
https://www.nsf.gov/awardsearch/showAward?AWD_ID=1908798&HistoricalAwards=false
关键词：
SHF Small Formalisms Implementations Verification

项目摘要

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.

真实的数的有效和精确表示是计算机科学中的一个基础问题。浮点数广泛用于使用有限位数来近似真实的数。鉴于需要良好的性能和挑战，在推理舍入误差或特殊条件下的浮点表示，有兴趣在社会上探索可能的替代品。Posit表示是最近提出的替代IEEE-754浮点表示。该项目开发技术，工具和程序，以确定是否Posit是一个可行的替代浮点。该项目的影响如下：（1）使程序员能够使用Posits有效地编写正确的程序，（2）为生成高性能数学库和Posits自动推理做出基础性进展，（3）影响科学计算领域的专家，减轻他们对正确性和准确性的担忧，以及（4）教育研究生，本科生，和高中生的基础抽象和推理技术。在相同的位数下，Posit表示可以比浮点表示更多的真实的数。根据配置，它可以表示浮点所能表示的每个真实的值。 Posit社区正试图找到Posit在精度、性能或存储方面优于浮点的特定应用。该项目开发技术，工具和程序，以推理使用Posits编写的应用程序的可行性，性能和准确性。具体到性能，该项目开发高性能的数学库的Posit表示，并探讨硬件支持的Posit操作。为了推理计算的准确性，研究人员开发了快速阴影执行技术，将Posit执行与真实的数字执行进行比较。为了使使用Posits的程序能够自动推理，该项目开发了一种可用于可满足性模理论求解器的Posits理论。该奖项反映了NSF的法定使命，并通过使用基金会的智力价值和更广泛的影响审查标准进行评估，被认为值得支持。

项目成果

期刊论文数量（9）

专著数量（0）

科研奖励数量（0）

会议论文数量（0）

专利数量（0）

Parallel Shadow Execution to Accelerate the Debugging of Numerical Errors

并行影子执行加速数值错误的调试

DOI：
10.1145/3468264.3468585
发表时间：
2021
期刊：
2021 The ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE
影响因子：
0
作者：
Chowdhary, Sangeeta;Nagarakatte, Santosh
通讯作者：
Nagarakatte, Santosh

Fast shadow execution for debugging numerical errors using error free transformations

使用无错误转换快速阴影执行来调试数值错误

DOI：
10.1145/3563353
发表时间：
2022
期刊：
Proceedings of the ACM on Programming Languages
影响因子：
0
作者：
Chowdhary, Sangeeta;Nagarakatte, Santosh
通讯作者：
Nagarakatte, Santosh

Approximating trigonometric functions for posits using the CORDIC method

使用 CORDIC 方法近似三角函数

DOI：
10.1145/3387902.3392632
发表时间：
2020
期刊：
CF '20: Proceedings of the 17th ACM International Conference on Computing Frontiers
影响因子：
0
作者：
Lim, Jay P;Shachnai, Matan;Nagarakatte, Santosh
通讯作者：
Nagarakatte, Santosh

Fast Polynomial Evaluation for Correctly Rounded Elementary Functions using the RLIBM Approach

使用 RLIBM 方法对正确舍入的初等函数进行快速多项式计算