SHF:Small:Concurrency In 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.