High-Level Abstractions for Safe Parallelism

Recent research efforts have developed sophisticated type systems for eliminating unwanted interference (i.e., read-write conflicts) from parallel code. While these systems are powerful, they suffer from potential barriers to adoption in that (1) they rely upon complex and/or restrictive features that may be difficult for programmers to understand and use; and (2) they impose a nontrivial annotation burden.

In this work we explore a different approach: instead of extending the type system to do all the work of proving noninterference, we rely upon high-level abstractionsthat capture important patterns of noninterfering parallelism — for example, performing a parallel divide-and-conquer update on an array, or updating different array cells in parallel while reading memory disjoint from the array. We show how, with suitably designed APIs, a few simple type system extensions can guarantee that user code is noninterfering, assuming the APIs are correctly implemented. Of course someone still must check the API implementation; but such checking (which can be done, e.g., with program logic) is hidden from the user of the API.

To illustrate the idea, we present a prototype implementation in Standard ML, including several parallel APIs and two realistic client programs. We sketch the typing annotations and verification methodology we have in mind. We pose several research questions raised by the prototype and suggest ideas for extending the work.