| Research |
| [ CSI ] [ ETH ] |
[ Lab Manager ]
| [ Publications ] [ Research Opportunities ] [ Partners & Supporters ] [ Earlier Work ] |
|
Intervals: Data-Race-Free Parallel Programming |
| Nicholas Matsakis, Intervals: Data-Race-Free Parallel Programming, Swiss Federal Institute of Technology, ETH Zurich. (Diss. ETH No. 19725), July 2011. [DISS_ETH_19725.pdf] |
| Experience has shown that thread-based parallel programming is prone to error. One particularly common kind of error is a data race. A data race occurs when multiple parallel, unordered threads access the same memory location, and at least one of those tasks is performing a write. Unfortunately, data races are not only common, they are also extremely challenging to debug. The difficulty arises because the outcome of such a race depends on the scheduler. As a result, a program can execute in dramatically different ways on every execution, making the problem difficult to reproduce and isolate. This dissertation proposes a two-part approach to preventing data races. The thesis begins by introducing a novel, more declarative abstraction for parallel programming called \emph{intervals}. Intervals replace threads and signals as the primary means of controlling what parts of the program may execute in parallel. The second part of the thesis is a modular type system that guarantees data-race freedom. This type system is based on intervals. Its distinguishing feature is that it tracks a static approximation of the program ordering at all times, which is then used to ensure that the various readers and writers of each field are always ordered. This allows the type system to check that lock-free programs are data-race-free. To evaluate the type system, we present three examples. These examples highlight different features of the type system and demonstrate its ability to represent real-world scenarios. The first example is a collection library; it shows how the intervals type system supports generic classes that can be used in many different ways. Using the intervals type system, it is possible to check both the mutable collections found in Java and the persistent (immutable) collections found in functional languages, as well as an interesting hybrid of the two, where collections are mutable for a specific period of time. The second example is a parallel compiler for the Featherweight Java language, where each class and method is compiled and type-checked in parallel. This example shows a non-trivial parallelization strategy that is nonetheless completely lock free. The final example is a parallel solver for the Traveling Salesman Problem, which demonstrates how locked and lock-free data can be combined. |
| [ Publications ] [ Research Opportunities ] [ Partners & Supporters ] [ Earlier Work ] |