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.