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

Bocchino, Robert L., Jr.

Permalink

https://hdl.handle.net/2142/18416 Copy

Description

Title

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

Author(s)

Bocchino, Robert L., Jr.

Issue Date

2011-01-14T22:50:09Z

Director of Research (if dissertation) or Advisor (if thesis)

Adve, Vikram S.

Doctoral Committee Chair(s)

Adve, Vikram S.

Committee Member(s)

• Padua, David A.
• Roşu, Grigore
• Snir, Marc
• Chamberlain, Bradford L.
• Grossman, Dan

Department of Study

Computer Science

Discipline

Computer Science

Degree Granting Institution

University of Illinois at Urbana-Champaign

Degree Name

Ph.D.

Degree Level

Dissertation

Keyword(s)

• parallel
• parallelism
• fork-join
• programming languages
• determinism
• nondeterminism
• regions
• effects
• effect systems
• effect checking
• strong isolation
• atomicity
• transactional memory
• atomic sections
• data race freedom
• frameworks

Abstract

This thesis presents a new, Java-based object-oriented parallel language 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). Those models 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 simplifies parallel programming. This thesis makes several broad contributions to the state of the art in programming languages and effect systems. First, it presents a comprehensive research agenda for achieving determinism by default in parallel languages with reference aliasing and shared mutable state. It argues that an object-oriented effect system is a good approach to managing shared memory conflicts. It also raises several technical challenges, many of which are taken up in the rest of the thesis. Second, this thesis presents an effect system and language for deterministic parallel programming using a fork-join model of parallel control. 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 deterministic parallelism that previous systems cannot express. We describe the effect system and language both formally and informally, and prove soundness for the formal language. We also describe our evaluation showing that the language can express a range of parallel programming patterns with good performance. Third, this thesis extends the effect system and language for determinism to support a controlled form of nondeterminism. Conflicting accesses are allowed only for an explicitly identified nondeterministic parallel construct, so the language is deterministic by default. A transactional runtime provides isolation for atomic statements, while the extended effect system provides stronger compile-time safety guarantees than any system we know of. In addition to determinism by default, the language guarantees race freedom; strong isolation for atomic statements even if the runtime guarantees only weak isolation; and an elegant way of composing 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 system enables 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, for example pipeline parallelism. We show how to write a framework API using the DPJ effect system so that the framework writer can guarantee correctness properties to the user, assuming the user's code passes the DPJ type checker. We also show how to extend the DPJ effect system to add generic types and effects, making the frameworks more general 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 parallel algorithms.

Graduation Semester

2010-12

Permalink

http://hdl.handle.net/2142/18416

Copyright and License Information

© 2010 Robert L. Bocchino Jr. Chapters 3 and 5 are derived from work published in ACM conference proceedings (OOPSLA 2009 and POPL 2011). As to that work only, the following notice applies: Copyright © 2009, 2011 by the Association for Computing achinery, Inc. Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, to republish, to post on servers, or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from Publications Dept., ACM, Inc., fax +1 (212) 869-0481, or permissions@acm.org.

Owning Collections