SHF: Medium: Algorithmic lambda-Calculus for the Design, Analysis, and Implementation of Parallel Algorithms

近年来硬件的进步使多核芯片和并行计算成为主流。虽然在过去的十年中，在多核芯片的并行软件方面取得了许多进展，但仍然没有令人满意的模型来分析并行算法的性能。特别是，与顺序算法的情况不同，用于估计算法性能的成本模型与用于实现算法的易于使用的编程模型之间存在差距。这个项目正在开发一种实用的并行算法方法，将两种基本但不同的计算理论结合在一起——一种基于机器模型，并遵循阿兰·图灵博士的工作，另一种基于语言模型，并遵循阿朗佐·丘奇博士的工作。该项目的新颖之处在于将这两种理论结合在一起，目前这两种理论存在很大的分歧。该项目的影响是在简化并行算法的设计和分析方面迈出了重要的一步，并更好地理解了两种计算理论之间的关系。该项目的教育部分包括教授本科生并行算法，并创造充足的机会来测试所提出方法的实际有效性，同时通过卡内基-梅隆大学的项目，具体努力扩大对计算的参与。这项工作遵循端到端的方法，将丘奇和图灵的理论与实践联系起来。在理论方面，该项目正在开发一种称为“算法λ演算”的演算，该演算为Church的λ演算提供了成本语义，使其能够推断程序的总工作和并行跨度（时间），从而可以用来理解算法的性能，至少是渐进的。为了证明这种演算是可实现的，该项目在理论上建立了演算忠实于转换语义，然后可以在并行ram等抽象机器上有效地实现。在实践方面，该项目正在开发一种忠实地实现这一理论的编程语言和编译器。该项目还扩展了算法lambda-calculus、可实现性定理和实现，以支持诸如聚合并行数据结构、交互和不同形式的并行性等重要特性。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

The hardware advances of recent years have brought multicore chips and parallel computing to the mainstream. While there have been many advances in parallel software for such multicore chips over the past decade, there is still no satisfactory model for analyzing the performance of parallel algorithms. In particular, and unlike the case for sequential algorithms, there is a gap between cost models for estimating performance of algorithms and easy to use programming models for implementing the algorithms. This project is developing a practical approach to parallel algorithms by bringing together two fundamental but distinct theories of computing---one based on machine models and following the work that dates back to Dr. Alan Turing, and the other based on language models and following the work that dates back to Dr. Alonzo Church. The novelty of the project is in combining these two theories, for which there is currently a large rift. The impact of the project is in making significant steps in simplifying the design and analysis of parallel algorithms, and better understanding of the relationship between the two theories of computing. The educational component of this project involves teaching undergraduates parallel algorithms and creates ample opportunities to test the practical effectiveness of the proposed approach, along with concrete efforts to broaden participation in computing through programs at Carnegie-Mellon University.The work is following an end-to-end methodology bridging Church and Turing's theories along with practice. On the theory side, the project is developing a calculus called the ``algorithmic lambda-calculus,'' that equips Church's lambda-calculus with a cost semantics, making it possible to reason about the total work and parallel span (time) of programs, which in turn can be used to understand the performance of algorithms, at least asymptotically. To show that this calculus is realizable, the project is theoretically establishing that the calculus is faithful to a transition semantics, which can then be efficiently realized on an abstract machine such as the Parallel-RAM. On the practical side, the project is developing a programming language and a compiler that faithfully implements this theory. The project is also extending the algorithmic lambda-calculus, the realizability theorems, and the implementation to support important features such as aggregate parallel data structures, interaction, and different forms of parallelism.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.