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.
Speculative execution either by intent or through misfortune (in response to error conditions) is pervasive in system design and yet it remains difficult to handle at the program level. The state of the art in "speculative distributed computing" is that: * speculation is the norm in practical distributed algorithms; * speculative algorithms are intricate to write and hard to reason about because speculative computations usually intermingle the various execution paths with concurrency and communication in an unprincipled way; * a theory of speculation should tease apart these various aspects. Specifically the speculation, the speculative algorithm, and its backup should all be first class separate citizens of a distributed computation. We find that despite the importance of speculative computation, there is very little programmatic support for it in distributed languages at the foundational level it deserves. From a programming language perspective, speculative execution requires a backtracking mechanism. Even in the sequential case, backtracking in the presence of various computational effects (e.g. assignments, exceptions, etc.) has significant subtleties. The introduction of concurrency additionally requires a "distributed backtracking" algorithm that must "undo" the effects of any communication events that occurred in the scope over which we wish to backtrack. In this project, we introduced a programming model for a distributed language with message-passing concurrency that treats "speculation" as a first class construct. The focus on message-passing concurrency is justified by the emergence of massively parallel multicore processors with high-bandwidth message passing. In this domain, speculative execution can be used to eliminate sequential bottlenecks by performing work ahead of synchronization constraints and discarding this speculative work if it violates consistency requirements. The key contributions of this project are a protocol for handling point-to-point synchronous communication that enables a clean implementation of scoped rollback in a distributed program; a formal model of the protocol with automated verification; and the design of a high-level concurrent reversible language that embodies this protocol and its implementation in Scala.
