SHF: Small: Reversible Concurrency

点击翻译按钮获取中文摘要

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.