SHF: Small: Reversible Concurrency

我们面临着这样一个未来：处理器级别的计算资源是“免费的”，有数百或数千个内核，但除了结构良好和高度并行的应用程序之外，我们几乎不知道如何利用这些资源。从长远来看，这项研究的目的是为程序员提供与《自然》杂志利用同样的计算能力来有效地解决难题。《自然》杂志中占主导地位的编程模型是大量“廉价”计算元素通过消息传递进行协作。解决复杂问题的一种策略是推测性地并行地寻求许多可能的解决方案，放弃缺乏希望或违反必要约束的（部分）计算。不幸的是，并发推测算法的开发具有挑战性，因为执行路径与并发性和通信混合在一起。这个项目的目标是朝着并发算法的推测理论迈出重要的一步，并为它们的发展开发一个实验框架。这项研究将使研究新的应用程序能够利用未来处理器似乎注定要提供的大量计算资源。这个项目的灵感和信息来自于最近关于可逆计算的工作，而可逆计算本身的灵感来自于物理定律中的可逆性。对可逆并发性的研究，虽然阐明了系统必须满足的关键属性（例如，通信的因果解除），但既没有产生可以在分布式环境中合理实现的模型，也没有为实用语言提供必要的细节。该项目将开发并发编程语言，支持并发系统中的显式推测，使用可逆并发编程的思想来提出用于从推测算法中实现推测的机制。该项目还将利用回溯monad和monad转换器的想法来隔离推测和计算效果（包括通信）之间的相互作用，并利用过程代数的想法来开发一个模型，用于理解支持推测执行的语言结构。研究包括实现和测试语言结构的实验工作，以及为这些结构提供正式模型的理论工作，以及能够对利用它们的程序进行推理的代数工具。

We face a future in which computational resources at the processor level are "free" with hundreds or thousands of cores, yet we have little idea how to utilize these resources except for well-structured and highly parallel applications. This research aims, in the long term, to provide programmers with the same computing power that Nature exploits to seemingly solve difficult problems efficiently. The dominant programming model in Nature is that of a massive number of "cheap" computing elements collaborating by message passing. One such strategy to solving complex problems is to speculatively pursue many possible solutions in parallel, discarding (partial) computations that lack promise or violate necessary constraints. Unfortunately concurrent speculative algorithms are challenging to develop because of the intermingling of execution paths with concurrency and communication. The goal of this project is to take significant steps towards a theory of speculation for concurrent algorithms and to develop an experimental framework for their development. This research will enable the study of novel applications to utilize the vast computational resources that future processors seem destined to provide.This project is inspired and informed by recent work on reversible computing which is itself inspired by reversibility in the laws of Physics. Research on reversible concurrency, while illuminating key properties that a system must satisfy (e.g. causal unwinding of communication), has neither yielded models that can reasonably be implemented in a distributed environment nor provided necessary details for a practical language. This project will develop concurrent programming languages that support explicit speculation in concurrent systems using the ideas from reversible concurrent programming to factor out the mechanisms used to realize speculation from speculative algorithms. The project will also leverage ideas from backtracking monad and monad transformers to isolate the interactions between speculation and computation effects including communication, and ideas from process algebras to develop a model for understanding language constructs supporting speculative execution. The research includes experimental work to implement and test linguistic constructs and theoretical work to provide both formal models for these constructs, and algebraic tools to enable reasoning about programs that utilize them.