An effect system and language for deterministic-by-default parallel programming

摘要

This thesis presents a new, Java-based object-oriented parallellanguage called Deterministic Parallel Java (DPJ). DPJ uses a novel effect system to guarantee determinism by default. That means that parallel programs are guaranteed to execute deterministically unless nondeterminism is explicitly requested. This is in contrast to the shared-memory models in widespread use today, such as threads and locks (including threads in ordinary Java). Thosemodels are inherently nondeterministic, do not provide any way to check or enforce that a computation is deterministic, and can even have unintended data races, which can lead to strange and unexpected behaviors. Because deterministic programs are much easier to reason about than arbitrary parallel code, determinism by default simplifiesparallel programming.This thesis makes several broad contributions to the state of the art in programming languages and effect systems. First, itpresents a comprehensive research agenda for achieving determinism bydefault in parallel languages with reference aliasing and sharedmutable state. It argues that an object-oriented effect system is agood approach to managing shared memory conflicts. It also raisesseveral technical challenges, many of which are taken up in the restof the thesis.Second, this thesis presents an effect system and language fordeterministic parallel programming using a fork-join model of parallelcontrol. With simple modular checking, and with no runtime checking overhead, the effect system guarantees at compile time that there are no conflicting memory accesses between any pairs of parallel tasks. The effect system supports several important patterns of deterministicparallelism that previous systems cannot express. We describe theeffect system and language both formally and informally, and provesoundness for the formal language. We also describe our evaluationshowing that the language can express a range of parallel programming patterns with good performance.Third, this thesis extends the effect system and language fordeterminism to support a controlled form of nondeterminism. Conflicting accesses are allowed only for an explicitly identifiednondeterministic parallel construct, so the language is deterministic by default. A transactional runtime provides isolation for atomicstatements, while the extended effect system provides strongercompile-time safety guarantees than any system we know of. Inaddition to determinism by default, the language guarantees racefreedom; strong isolation for atomic statements even if the runtime guarantees only weak isolation; and an elegant way ofcomposing deterministic and nondeterministic operations that preserves local reasoning about deterministic operations. Again we give an informal treatment, a formal treatment, and soundness proofs. We describe an evaluation showing that the extended language can express realistic nondeterministic algorithms in a natural way, with reasonable performance given the transactional runtime we used. Further, by eliminating unnecessary synchronization, the effect systemenables a significant reduction in the software runtime overhead.Fourth, this thesis describes programming techniques and further extensions to the effect system for supporting object-oriented parallel frameworks. Frameworks represent an important tool for parallel programming in their own right. They can also express some operations that the language and effect system alone cannot, forexample pipeline parallelism. We show how to write a framework APIusing the DPJ effect system so that the framework writer can guaranteecorrectness properties to the user, assuming the user's code passesthe DPJ type checker. We also show how to extend the DPJ effectsystem to add generic types and effects, making the frameworks moregeneral and useful. Finally, we state the requirements for a correct framework implementation. These requirements may be checked with a combination of DPJ's effect system and external reasoning. Again we give an informal treatment, a formal treatment, and soundness proofs. We also describe the results of an evaluation showing that the techniques described can express realistic frameworks and parallelalgorithms.