behaviors of parallel programs directly and easily. Specifically, we should provide an assertion framework where programmers can directly and precisely express intended deterministic behavior. Further, the framework should be flexible enough so that deterministic behaviors can be expressed more easily than with a traditional assertion framework. For example, when expressing the deterministic behavior of a parallel edge detection algorithm for images, we should not have to rephrase the problem as race detection; nor should we have to write a state assertion that relates the output to the input, which would be complex and time-consuming. Rather, we should simply be able to say that, if the program is executed on the same input image, then the output image remains the same regardless of how the program’s parallel threads are scheduled.

In this paper, we propose such a framework for asserting that blocks of parallel code behave deterministically. Formally, our framework allows a programmer to give a specification for a block P of parallel code as:

deterministic assume(Pre(s0,s¢0) ) {

P

} assert(Post(s, s¢));

This specification asserts the following: Suppose P is executed twice with potentially different schedules, once from initial state s0 and once from s¢0 and yielding final states s and s ¢. Then, if the user-specified precondition Pre holds over s0 and s ¢0, then s and s¢ must satisfy the user-specified postcondition Post.

For example, we could specify the deterministic behavior of a parallel matrix multiply with:

deterministic assume(|A − A¢| < 10− 9 and
C = parallel_matrix_multiply_float(A, B);
} assert(|C − C¢| < 10− 6);

Note the use of primed variables A¢,B¢, and C¢ in the above example. These variables represent the state of the matrices A,B,and C from a different execution. Thus, the predicates that we write inside assume and assert are different from state predicates written in a traditional assertion framework— our predicates relate a pair of states from different executions. We call such predicates bridge predicates and assertions using bridge predicates bridge assertions. A key contribution of this paper is the introduction of these bridge predicates and bridge assertions.

Our deterministic assertions provide a way to specify the correctness of the parallelism in a program independently of the program’s traditional functional correctness. By checking whether different program schedules can nondeterministically lead to semantically different answers, we can find bugs in a program’s use of parallelism even when unable to directly specify or check functional correctness—i.e., that the program’s output is correct given its input. Inversely, by checking that a parallel program behaves deterministically, we can gain confidence

98 communications of the acm | JunE 2010 | VoL. 53 | no. 6

in the correctness of its use of parallelism independently of whatever method we use to gain confidence in the program’s functional correctness.

We have implemented our deterministic assertions as a library for the Java programming language. We evaluated the utility of these assertions by manually adding deterministic specifications to a number of parallel Java benchmarks. We used an existing tool to find executions exhibiting data and higher-level races in these benchmarks and used our deterministic assertions to distinguish between harmful and benign races. We found it to be fairly easy to specify the correct deterministic behavior of the benchmark programs using our assertions, despite being unable in most cases to write traditional invariants or functional correctness assertions. Further, our deterministic assertions successfully distinguished the two races known to lead to undesired nondeterminism from the benign races in the benchmarks.

2. DeteRministic sPecification

In this section, we motivate and define our proposal for assertions for specifying determinism.

Strictly speaking, a block of parallel code is said to be deterministic if, given any particular initial state, all executions of the code from the initial state produce the exact same final state. In our specification framework, the programmer can specify that they expect a block of parallel code, say P, to be deterministic with the following construct:

deterministic {
P
}

This assertion specifies that if s and s¢ are both program states resulting from executing P under different thread schedules from some initial state s0, then s and s¢ must be equal. For example, the specification:

deterministic {
C = parallel_matrix_multiply_int(A, B);
}

asserts that for the parallel implementation of matrix multiplication in function parallel_matrix_multiply_ int, any two executions from the same program state must reach the same program state—i.e., with identical entries in matrix C—no matter how the parallel threads are scheduled.

A key implication of knowing that a block of parallel code is deterministic is that we may be able to treat the block as sequential in other contexts. That is, although the block may have internal parallelism, a programmer (or perhaps a tool) can hopefully ignore this parallelism when considering the larger program using the code block. For example, perhaps a deterministic block of parallel code in a function can be treated as if it were a sequential implementation when reasoning about the correctness of code calling the function.