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

SHF:Small:Concurrency In Reversible Computations

SHF:Small:可逆计算中的并发

基本信息

批准号：
2242786
负责人：
Clement Aubert
金额：
$ 58.26万
依托单位：
AUGUSTA UNIVERSITY RESEARCH INSTITUTE, INC.
依托单位国家：
美国
项目类别：
Standard Grant
财政年份：
2023
资助国家：
美国
起止时间：
2023-03-01 至 2026-02-28
项目状态：
未结题

来源：
https://www.nsf.gov/awardsearch/showAward?AWD_ID=2242786&HistoricalAwards=false
关键词：
SHF Small Concurrency Reversible Computations

项目摘要

Most computers today are designed to operate unidirectionally, but novel adiabatic, quantum, and biological computers require bidirectional, that is, forward and backward flow of computations, because such computations are reversible in nature. Such novel technologies have already started to revolutionize not only the very essence of computing, but also of communicating. The communication protocols they utilize are drastically different from the ones currently in use, and much more complex, since the protocols must account for the possibility that any participant may undo any computation. This project provides a complete and satisfactory set of definitions to specify reversible protocols, demonstrate their equivalence, and reason about independent events. The project's novelties are to propose direction-agnostic definitions whenever possible, treating backward and forward executions as equal, and to leverage reversibility to question choices inherited from forward-only formalisms. The project's impacts are in the development and adoption of reversible languages, that will allow the creation of energy-efficient systems and protocols; but also improve security and reliability thanks to built-in forensic capabilities.This project concurrently refines the definition of independence for reversible systems; implements a specification language for reversible systems; enriches current definitions of contextual equivalences; and strives to take inspiration from different fields to strike "the right" set of operators to represent reversible communications. The project's advances include a greater homogeneity between the different representations of reversible protocols, a better insight into the principled development of reversible languages, and a better integration between the formalism used to specify protocols and its application to reasoning about modern reversible systems.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.

今天的大多数计算机都被设计为单向操作，但新型的绝热、量子和生物计算机需要双向的，即向前和向后的计算流，因为这些计算在本质上是可逆的。这些新技术不仅已经开始彻底改变计算的本质，而且也开始改变通信的本质。他们使用的通信协议与目前使用的协议有很大的不同，而且要复杂得多，因为协议必须考虑到任何参与者都可能撤销任何计算的可能性。这个项目提供了一套完整的和令人满意的定义来指定可逆协议，证明它们的等价性，并对独立事件进行推理。该项目的新颖之处是尽可能提出方向不可知的定义，将向后和向前执行视为平等，并利用可逆性来质疑从仅向前形式主义继承的选择。该项目的影响在于可逆语言的开发和采用，这将允许创建节能系统和协议;而且由于内置的取证功能，还可以提高安全性和可靠性。该项目同时细化了可逆系统的独立性定义;实现了可逆系统的规范语言;丰富了当前上下文等效项的定义;并努力从不同领域获得灵感，以找到“正确的”运算符集合来表示可逆通信。该项目的进步包括可逆协议的不同表示之间更大的同质性，更好地洞察可逆语言的原则性发展，该奖项反映了NSF的法定使命，并被认为值得通过使用基金会的智力价值和更广泛的影响审查标准。