Asserting and Checking
Determinism for
Multithreaded Programs

abstract

The trend towards processors with more and more parallel cores is increasing the need for software that can take advantage of parallelism. The most widespread method for writing parallel software is to use explicit threads. Writing correct multithreaded programs, however, has proven to be quite challenging in practice. The key difficulty is nondeterminism. The threads of a parallel application may be interleaved nondeterministically during execution. In a buggy program, nondeterministic scheduling can lead to nondeterministic results—where some interleavings produce the correct result while others do not.

We propose an assertion framework for specifying that regions of a parallel program behave deterministically despite nondeterministic thread interleaving. Our framework allows programmers to write assertions involving pairs of program states arising from different parallel schedules. We describe an implementation of our deterministic assertions as a library for Java, and evaluate the utility of our specifications on a number of parallel Java benchmarks. We found specifying deterministic behavior to be quite simple using our assertions. Further, in experiments with our assertions, we were able to identify two races as true parallelism errors that lead to incorrect nondeterministic behavior. These races were distinguished from a number of benign races in the benchmarks.

1. intRoDuction

The semiconductor industry has hit the power wall— performance of general-purpose single-core microprocessors can no longer be increased due to power constraints. Therefore, to continue to increase performance, the microprocessor industry is instead increasing the number of processing cores per die. The new “Moore’s Law” is that the number of cores will double every generation, with individual cores going no faster. 2

This new trend of increasingly parallel chips means that we
will have to write parallel software in order to take advantage
of future hardware advances. Unfortunately, parallel software
is more difficult to write and debug than its sequential coun-
terpart. A key reason for this difficulty is nondeterminism—i.e.,
that in two runs of a parallel program on the exact same input,
the parallel threads of execution can interleave differently,
producing different output. Such nondeterministic thread
interleaving is an essential part of harnessing the power of
parallel chips, but it is a major departure from sequential
programming, where we typically expect programs to behave
identically in every execution on the same input. We share a
widespread belief that helping programmers manage nonde-
terminism in parallel software is critical in making parallel
programming widely accessible.

The original version of this paper was published in Proceedings of the 7th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, August 2009.