SHF: Small: Generalizing Monotonic Data Structures for Expressive, Deterministic Parallel Programming

当前计算机硬件的趋势是并行、独立处理单元（核心）的数量不断增加。这种趋势需要从传统的顺序编程向并行编程的广泛过渡。但由于并行编程是出了名的困难，采用一直缓慢。造成这种困难的一个根本原因是，由于并行任务之间不可预测的交互，程序经常会产生不一致的答案，甚至崩溃。然而，某些类别的程序承认强有力的数学保证，即使并行执行，它们也会表现相同。这项研究扩展了这种确定性程序的数学基础。它研究了一系列编程语言，这些语言既允许并行计算，又允许以对共享数据的有限修改和观察的形式在它们之间进行通信。所允许的通信比该领域以前的工作具有更广泛的性质。该项目围绕lambda演算的一种变体展开，它包括共享变量，这些变量的状态占据一个连接半格，并在该半格内单调变化。许多确定性编程模型，包括最近的（Intel CnC）和较早的（Kahn-MacQueen Process Networks），都可以映射到这个框架中。除了为语言构建决定论的证明之外，该项目还探索了各种扩展，包括有限形式的非决定论（即，承认失败但从不错误答案）。最后，本项目将使用其形式语言作为对实际并行程序进行推理的工具。也就是说，可以通过验证程序的共享状态形成半格和状态变化是单调的来证明决定论。

The current trend in computer hardware is towards increasing numbers of parallel, independent processing units (cores). This trend necessitates a widespread transition from traditional sequential programming to parallel programming. But because parallel programming is notoriously difficult, adoption has been slow. A fundamental reason for this difficulty is that programs can often yield inconsistent answers, or even crash, due to unpredictable interactions between parallel tasks. Certain classes of programs, however, admit strong mathematical guarantees that they will behave the same in spite of parallel execution. This research is extending the mathematical foundation underlying such deterministic programs. It studies a family of programming languages that allow both parallel computations, and communications between them in the form of restricted modifications to, and observations of, shared data. The communication allowed is of a more general nature than previous work in the area.This project is centered around a variant of the lambda-calculus that includes shared variables whose states occupy a join semilattice and change monotonically within that lattice. A number of deterministic programming models, both recent (Intel CnC), and older (Kahn-MacQueen Process Networks), can be mapped into this framework. In addition to constructing proofs of determinism for the language, this project explores various extensions, including limited forms of nondeterminism (i.e., which admit failures but never wrong answers). Finally this project will use its formal language as a tool for reasoning about practical parallel programs. That is, determinism can be demonstrated by verifying that the program's shared states form a semilattice and state changes are monotonic.