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-calculus的变体围绕，其中包括共享变量，其状态占据了联盟半静脉，并在该晶格中单调更改。 可以将许多确定性的编程模型（Intel CNC）和较旧的（Kahn-Macqueen Process网络）映射到此框架中。 除了构建语言的确定性证明外，该项目还探讨了各种扩展，包括有限的非确定性形式（即承认失败但从未错误的答案）。 最后，该项目将使用其正式语言作为推理实用平行程序的工具。 也就是说，可以通过验证程序的共享状态形成半层次和状态变化是单调的，可以证明确定性。