a single program state, and a postcondition is usually written over two states—the states at the beginning and end of the function. For example:

 

parallel_matrix_multiply_int(A, B) { assume( A.cols == B.rows);

... assert(C == A × B); return C;

}

The key difference between a postcondition and a Post predicate is that a postcondition relates two states at different times along a same execution—e.g., here relating inputs A and B to output C—whereas a Post predicate relates two program states from different executions.

Advantages of Deterministic Assertions: Our deterministic specifications are a middle ground between the implicit specification used in race detection—that programs should be free of data races—and the full specification of functional correctness. It is a great feature of data race detectors that typically no programmer specification is needed. However, manually determining which reported races are benign and which are bugs can be time-consuming and difficult. We believe our deterministic assertions, while requiring little effort to write, can greatly aid in distinguishing harmful from benign data races (or higher-level races).

One could argue that a deterministic specification framework is unnecessary given that we can write the functional correctness of a block of code using traditional pre- and postconditions. For example, one could write the following to specify the correct behavior of a paralell matrix multiply:

C = parallel_matrix_multiply_float(A, B); assert(|C − A × B| < 10− 6);

We agree that if one can write a functional specification of a block of code, then there is no need to write deterministic specification, as functional correctness implies deterministic behavior.

The advantage of our deterministic assertions is that they provide a way to specify the correctness of just the use of parallelism in a program, independent of the program’s full functional correctness. In many situations, writing a full specification of functional correctness is difficult and time-consuming. A simple deterministic specification, however, enables us to use automated techniques to check for parallelism bugs, such as harmful data races causing semantically nondeterministic behavior.

Consider a function parallel_edge_detection that takes an image as input and returns an image where detected edges have been marked. Relating the output to the input image with traditional pre- and postconditions would likely be quite challenging. However, it is simple to specify that the routine does not have any parallelism bugs causing a correct image to be returned for some thread schedules and an incorrect image for others:

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

deterministic assume(img.equals(img¢)) { result = parallel_edge_detection(img);

} assert(result.equals(result¢));

 

where img.equals(img¢) returns true if the two images are pixel-by-pixel equal.

For this example, a programmer could gain some confidence in the correctness of the routine by writing unit tests or manually examining the output for a handful of images. He or she could then use automated testing or model checking to separately check that the parallel routine behaves deterministically on a variety of inputs, gaining confidence that the code is free from concurrency bugs.

We believe that it is often difficult to come up with effective functional correctness assertions. However, it is often quite easy to use bridge assertions to specify deterministic behavior, enabling a programmer to check for harmful concurrency bugs. In Section 5, we provide several case studies to support this argument.

3. checKinG DeteRminism

There may be many potential approaches to checking or verifying a deterministic specification, from testing to model checking to automated theorem proving. In this section, we propose a simple, sound, and incomplete method for checking deterministic specifications at run-time.

The key idea of the method is that, whenever a deterministic block is encountered at run-time, we can record the program states spre and spost at the beginning and end of the block. Then, given a collection of (spre, spost) pairs for a particular deterministic block in some program, we can check a deterministic specification by comparing pairwise the pairs of initial and final states for the block. That is, for a deterministic block:

deterministic assume(Pre) {
P
} assert(Post);

with pre- and postbridge predicates Pre and Post, we check for every recorded pair of pairs (spre, spost) and (s¢pre, s¢post) that:

Pre (spre, s¢pre) Þ Post (spost, s¢post)

If this condition does not hold for some pair, then we report a determinism violation.

To increase the effectiveness of this checking, we must record pairs of initial and final states for deterministic blocks executed under a wide variety of possible thread interleavings and inputs. Thus, in practice we likely want to combine our deterministic assertion checking with existing techniques and tools for exploring parallel schedules of a program, such as noise making, 7, 18 active random scheduling, 16 or model checking. 20

In practice, the cost of recording and storing entire program states could be prohibitive. However, real determinism