SHF: Small: Reversible Concurrency

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

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.