technical Perspective
Building confidence in
multicore software
By Vivek Sarkar

sUrPrises MAy Be fun in real life, but not so in software. One approach to avoiding surprises in software is to establish its functional correctness, either by construction or by verification, but this is feasible in only a limited set of domains. Instead, the predominant method in single-threaded software development has been an iterative approach of design, coding, testing, and bug fixes. The cornerstone of this practice is determinism; that is, the expectation a program will exhibit the same behavior each time it is executed with the same inputs. Even if a program has a bug, it is comforting to know the buggy behavior can be reproduced by others, and work-arounds can be shared until the developer provides a fix.

In this context, multithreaded programs prove to be more challenging to handle than single-threaded programs. For decades multithreaded programs were executed on single-core processors and users became accustomed to deterministic sets of behaviors exhibited by standard thread schedulers. However, the move to multicore hardware has completely changed this landscape, which is why I recommend you read the following paper.

Jacob Burnim and Koushik Sen
propose an assertion framework for
specifying regions of multithreaded
software that are expected to behave
deterministically, and describe a run-
time library for checking these asser-
tions that is guaranteed to be sound.
Though the proposed runtime check-
ing is incomplete in general, prelimi-
nary evaluations suggest that this ap-
proach can be effective in identifying
many common sources of nondeter-
minism. Runtime assertion-checking
is used in many situations nowadays,
including null-pointer, array-bounds
checks, and type checks in managed
runtimes. So, it is reasonable to view
the checking assertions related to de-
terminism as a natural future exten-
sion to the runtime checks performed
in modern software.

a key challenge in
multicore programs
is that determinism
lies in the eye of
the beholder.

postconditions (“assert” clauses) by using bridge predicates. A bridge predicate relates values arising from two different executions of the same program, thereby providing the foundation for asserting semantic determinism at any desired level of user-specified granularity. One of the examples discussed is parallel matrix multiply, where the bridge predicate in the precondition assumes the input matrices from two executions differ entry-by-entry by no more than an error threshold, and the bridge predicate in the postcondition asserts that a similar property holds for the output matrices. Note that these assertions are focused on determinism and not on functional correctness. For example, a functionally incorrect implementation of parallel matrix multiply that returns the identity matrix for all inputs will always pass determinism checking.

At this point I hope I’ve raised a number of questions in your mind. Can the determinism assertions be generated automatically? What is the relationship between checking assertions for determinism and detection of data races? Are there any assumptions made about the underlying system software and hardware, such as the memory consistency model? Can the programming constructs advocated by transactional memory researchers help address this problem? Are there applications of determinism assertions to single-threaded programs? If you’re interested in any of these questions, you need to read the following paper to better understand the ramifications of parallel hardware on determinism guarantees in multithreaded software!

 

Vivek Sarkar ( [e-mail]) is an ACM Fellow and a professor of computer science and of electrical and computer engineering at Rice university, where he holds the E.D. butcher Chair in Engineering.