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.
