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

SHF：小：泛化单调数据结构以实现富有表现力、确定性的并行编程

• 批准号: 1218375
• 负责人: Ryan Newton
• 金额: $ 37.73万
• 依托单位: Indiana University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2012
• 资助国家: 美国
• 起止时间: 2012-08-01 至 2015-07-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1218375&HistoricalAwards=false
• 关键词: SHF; Small; Generalizing; Monotonic; Data

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.

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