The third column of Table 1 records the number of
lines of specification (and lines of custom predicate code)
added to each benchmark. Overall, the specification burden is quite small. Indeed, for the majority of the programs,
an author was able to add deterministic assertions in only
5 to 10minutes per benchmark, despite being unfamiliar
with the code. In particular, it was typically not difficult to
both identify regions of code performing parallel computation and to determine from documentation, comments, or
source code which results were intended to be deterministic. Figure 2 shows the assertions added to the mandelbrot
The added assertions were correct on the first attempt for
all but two benchmarks. For phylogeny, the resulting phylogenetic tree was erroneously specified as deterministic,
when, in fact, there are many correct optimal trees. The specification was modified to assert only that the optimal score
must be deterministic. For sparsematmult, we incorrectly
identified the variable to which the output was written. This
error was identified during later work on automatically inferring deterministic specifications. 6
The two predicates provided by our assertion library were
sufficient for all but one of the benchmarks. For the JGF
montecarlo benchmark, the authors had to write a custom
equals and hashCode method for two classes— 34 total
lines of code—in order to assume and assert that two sets,
one of initial tasks and one of results, are equivalent across
Discussion: More experience, or possibly user studies, would
be needed to conclude decisively that our assertions are easier to use than existing techniques for specifying that parallel
code is correctly deterministic. However, we believe our experience is quite promising. In particular, writing assertions for
the full functional correctness of the parallel regions of these
programs seemed to be quite difficult, perhaps requiring
implementing a sequential version of the code and asserting
that it produces the same result. Further, there seemed to be
no obvious simpler, traditional assertions that would aid in
catching nondeterministic parallelism.
Despite these difficulties, we found that specifying the
natural deterministic behavior of the benchmarks with our
bridge assertions required little effort.
5. 2. effectiveness
To evaluate the utility of our deterministic specifications in
finding true parallelism bugs, we used a modified version
of the CalFuzzer14, 16 tool to find real races in the benchmark programs, both data races and higher level races (such
as races to acquire a lock). For each such race, we ran 10
trials using CalFuzzer to create real executions with these
races and to randomly resolve the races (i.e., randomly pick
a thread to “win”). We turned on run-time checking of our
deterministic assertions for these trials, and recorded all
Table 1 summarizes the results of these experiments. For
each benchmark, we indicate the number of real data races
and higher-level races we observed. Further, we indicate
how many of these races led to determinism violations in
In these experiments, the primary computational cost
is from CalFuzzer, which typically has an overhead in the
range of 2x–20x for these kinds of compute bound applications. We have not carefully measured the computational
cost of our deterministic assertion library. For most benchmarks, however, the cost of serializing and comparing a
computation’s inputs and outputs is dwarfed by the cost of
the computation itself—e.g., consider the cost of checking
that two fractal images are identical versus the cost of computing each fractal in the first place.
Determinism Violations: We found two cases of nondeterministic behavior. First, a known data race in the raytracer
benchmark, due the use of the wrong lock to protect a shared
sum, can yield an incorrect final answer.
Second, the pi benchmark can yield a nondeterministic
answer given the same random seed because of insufficient
synchronization of a shared random number generator.
In each Monte Carlo sample, two successive calls to java.
util.Random.nextDouble() are made. A context switch
between these calls changes the set of samples generated.
Similarly, nextDouble() itself makes two calls to java.
util.Random.next(), which atomically generates up to
32 pseudorandom bits. A context switch between these two
calls changes the generated sequence of pseudorandom
doubles. Thus, although java.util.Random.next-Double()is thread-safe and free of data races, scheduling
nondeterminism can still lead to a nondeterministic result.
(This behavior is known—the PJ Library provides several
versions of this benchmark, one of which does guarantee a
deterministic result for any given random seed.)
Benign races: The high number of real data races for these
benchmarks is largely due to benign races on volatile variables
used for synchronization—e.g., to implement a tournament
barrier or a custom lock. Although CalFuzzer does not understand these sophisticated synchronization schemes, our deterministic assertions automatically provide some confidence
that these races are benign because, over the course of many
experimental runs, they did not lead to nondeterministic final
Note that it can be quite challenging to verify by hand that
these races are benign. On inspecting the benchmark code
and these data races, an author several times believed he
had found a synchronization bug. But on deeper inspection,
the code was found to be correct in all such cases.
The number of high-level races is low for the JGF benchmarks because all the benchmarks except montecarlo
exclusively use volatile variables (and thread joins) for synchronization. Thus, all observable scheduling nondeterminism is due to data races.
The number of high-level races is low for the PJ benchmarks because they primarily use a combination of volatile variables and atomic compare-and-set operations for
synchronization. Currently, the only kind of high-level
race our modified CalFuzzer recognizes is a lock race.
Thus, while we believe there are many (benign) races
in the ordering of these compare-and-set operations,
CalFuzzer does not report them. The one high-level race
for pi, indicated in the table and described above, was
confirmed by hand.