Communications - June 2010

equal to within 2N ∑i|xi|, where Î is the machine epsilon. We can assert:

sum = parallel_sum(x); bound = 2 x.length  sum_of_abs(x); Predicate apx = new ApproxEquals(bound); Deterministic.assert(sum, apx);

As another example, different runs of a molecular dynamics simulation may be expected to produce particle positions equal to within something like  multiplied by the sum of the absolute values of all initial positions. We can similarly compute this value at the beginning of the computation, and use an ApproxEquals predicate with the appropriate bound to compare particle positions.

4. 2. concrete example: mandelbrot

Figure 2 shows the deterministic assertions we added to one of our benchmarks, a program for rendering images of the Mandelbrot Set fractal from the Parallel Java (PJ) Library. 11

The benchmark first reads a number of integer and floating-point parameters from the command-line. It then spawns several worker threads that each compute the hues for different segments of the final image and store the hues in shared array matrix. After waiting for all of the worker threads to finish, the program encodes and writes the image to a file given as a command-line argument.

To add determinism annotations to this program, we simply opened a deterministic block just before the worker threads are spawned and closed it just after they are joined. At the beginning of this block, we added an assume call for each of the seven fractal parameters, such as the image size and color palette. At the end of the block, we assert that the resulting array matrix should be deterministic, however the worker threads are interleaved.

Note that it would be quite difficult to add assertions
for the functional correctness of this benchmark, as each
pixel of the resulting image is a complicated function of the
inputs (i.e., the rate at which a particular complex sequence
diverges). Further, there do not seem to be any simple tra-
ditional invariants on the program state or outputs which
would help identify a parallelism bug.

5. eVaLuation

In this section, we describe our efforts to validate two claims about our proposal for specifying and checking deterministic parallel program execution:

1. First, deterministic specifications are easy to write. That is, even for programs for which it is difficult to specify traditional invariants or functional correctness, it is relatively easy for a programmer to add deterministic assertions.

2. Second, deterministic specifications are useful. When combined with tools for exploring multiple thread schedules, deterministic assertions catch real parallelism bugs that lead to semantic nondeterminism. Further, for traditional concurrency issues such as data races, these assertions provide some ability to distinguish between benign cases and true bugs.

To evaluate these claims, we used a number of benchmark programs from the Java Grande Forum (JGF) benchmark suite, 17 the Parallel Java (PJ) Library, 11 and elsewhere. The names and sizes of these benchmarks are given in Table 1. We describe the benchmarks in greater detail in Burnim and Sen. 5 Note that the benchmarks range from a few hundred to a few thousand lines of code, with the PJ benchmarks relying on an additional 10–20,000 lines of library code from the PJ Library (for threading, synchronization, and other functionality).

5. 1. ease of use

We evaluate the ease of use of our deterministic specification by manually adding assertions to our benchmark programs. One deterministic block was added to each benchmark.

table 1. summary of experimental evaluation of deterministic assertions. a single deterministic block specification was added to each benchmark. each specification was checked on executions with races found by the calfuzzer14, 16 tool.