CS Talk
April 24, 2012
10:30 a.m., AKW 200

Speaker: Robert Bocchino
Title: Deterministic Parallel Java

Abstract: With the proliferation of multicore computers on the desktop, parallel programming is becoming widespread, but it is still hard. One way to make it easier is to ensure that parallel programs are deterministic: that is, they produce the same output on every execution with a given input, regardless of the parallel schedule chosen. Determinism makes parallel programs much easier to write, understand, debug, and maintain. Further, many (though not all) parallel programs are intended to be deterministic. However, general-purpose languages — particularly those that allow updates to shared data, pointers, and aliasing — typically do not guarantee determinism. Instead, they require programmers to use testing, inspection, or some other method to ensure that their programs behave deterministically.

In this talk, I will present my Ph.D. thesis work on Deterministic Parallel Java (DPJ). DPJ is an explicitly parallel language based on Java. Like Java, it allows shared mutable objects and aliasing. However, it uses programmer annotations called effects to guarantee determinism by default: the program is guaranteed to run deterministically unless the programmer explicitly requests a controlled form of nondeterminism. Further, any nondeterminism is subject to strong safety guarantees, including freedom from data races and an intuitive way to compose deterministic and nondeterministic code. Finally, DPJ supports the encapsulation of common parallel patterns into easy-to-use frameworks that provide strong correctness guarantees.

I will give an overview of the typing mechanisms that DPJ uses to provide its guarantees, and I will illustrate some important parallel patterns that DPJ can express with good performance. I will conclude with a brief summary of work currently in progress on (1) making DPJ-style effect checking more flexible and powerful by adding a novel idea called "local uniqueness" and (2) integrating DPJ-style effect checking with Hoare-style reasoning, particularly for verifying framework implementations, where extra power is needed beyond what DPJ provides.

Bio: Robert Bocchino is a Postdoctoral Associate at Carnegie Mellon University and is supported by a CRA/CCC Computing Innovation Fellowship. His research interests lie in programming language design, type theory, formal verification, and concurrency. Robert completed his Ph.D. at the University of Illinois at Urbana-Champaign in fall 2010. His dissertation on Deterministic Parallel Java received the 2010 Outstanding Dissertation Award from ACM SIGPLAN and the 2012 David J. Kuck Outstanding Thesis Award from the University of Illinois.

At CMU, Robert is working with Jonathan Aldrich on the design and verification of high-level parallel abstractions using a combination of DPJ-style effects, unique references, and program logic. He has also contributed to the design of the type system in the Plaid language project. Plaid makes object states and transitions a first-class feature of the language, and its type system uses unique and immutable references to reason about object aliases.