Discussion: Although our checking of deterministic assertions
is sound—an assertion failure always indicates that two executions with equivalent initial states can yield nonequivalent
final states—it is incomplete. Parallelism bugs leading to nondeterminism may still exist even when testing fails to find any
determinism violations.
However, in our experiments we successfully distinguished the races known to cause undesired nondeterminism from the benign races in only a small number of trials.
Thus, we believe our deterministic assertions can help catch
harmful nondeterminism due to parallelism, as well as save
programmer effort in determining whether real races and
other potential parallelism bugs can lead to incorrect program behavior.
6. Discussion
In this section, we compare the concepts of atomicity and
determinism. Further, we discuss several other possible
uses for bridge predicates and bridge assertions.
Here we focus on atomicity and determinism as program specifications to be checked. There is much work
on atomicity as a language mechanism, in which an
atomic specification is instead enforced by some combination of library, run-time, compiler, or hardware
support. One could similarly imagine enforcing deterministic specifications through, e.g., compiler and run-time mechanisms. 4
6. 2. other uses of bridge predicates
We have already argued that bridge predicates simplify
the task of directly and precisely specifying deterministic
behavior of parallel programs. We also believe that bridge
predicates could provide a simple but powerful tool to
express correctness properties in many other situations.
For example, if we have two versions of a program, P1 and
P2, that we expect to produce the same output on the same
input, then we can easily assert this using our framework
as follows:
6. 1. atomicity versus determinism
A concept complementary to determinism in parallel programs is atomicity. A block of sequential code in a multithreaded program is said to be atomic9 if for every possible
interleaved execution of the program there exists an equivalent execution with the same overall behavior in which
the atomic block is executed serially (i.e., the execution of
the atomic block is not interleaved with actions of other
threads). Therefore, if a code block is atomic, the programmer can assume that the execution of the code block by a
thread cannot be interfered with by any other thread. This
enables programmers to reason about atomic code blocks
sequentially. This seemingly similar concept has the following subtle differences from determinism:
deterministic assume(Pre) {
if (nonDeterministicBoolean() ) {
P1
} else {
P2
}
} assert(Post);
where Pre requires that the inputs are the same and Post
specifies that the outputs will be the same.
In particular, if a programmer has written both a sequential
and parallel version of a piece of code, he or she can specify
that the two versions are semantically equivalent with an
assertion like:
1. Atomicity is the property about a sequential block of
code—i.e., the block of code for which we assert atomicity has a single thread of execution and does not
spawn other threads. Note that a sequential block is by
default deterministic if it is not interfered with by other
threads. Determinism is a property of a parallel block
of code. In determinism, we assume that the parallel
block of code’s execution is not influenced by the external world.
2. In atomicity, we say that the execution of a sequential
block of code results in the same state no matter how it is
scheduled with other external threads—i.e., atomicity
ensures that external nondeterminism does not interfere
with the execution of an atomic block of code. In determinism, we say that the execution of a parallel block of
code gives the same semantic state no matter how the
threads inside the block are scheduled—i.e., determinism ensures that internal nondeterminism does not result
in different outputs.
deterministic assume(A==A¢ and B==B¢) {
if (nonDeterministicBoolean() ) {
C = par_matrix_multiply_int(A, B);
} else {
C = seq_matrix_multiply_int(A, B);
}
} assert(C==C¢);
where nonDeterministicBoolean() returns true or
false nondeterministically.
Similarly, a programmer can specify that the old
and new versions of a piece of code are semantically
equivalent:
In summary, atomicity and determinism are orthogonal con-
cepts. Atomicity reasons about a single thread under external
nondeterminism, whereas determinism reasons about mul-
tiple threads under internal nondeterminism.
deterministic assume(A==A¢ and B==B¢) {
if (nonDeterministicBoolean() ) {
C = old_matrix_multiply_int(A, B);
} else {
C = new_matrix_multiply_int(A, B);
}
} assert(C==C¢);
