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

Carnegie Mellon University, Pittsburgh PA

Investigators

Abstract

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.