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 runtime library for checking these assertions that is guaranteed to be sound. Though the proposed runtime checking is incomplete in general, preliminary evaluations suggest that this approach can be effective in identifying many common sources of nondeterminism. 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 determinism as a natural future extension to the runtime checks performed in modern software.
A key challenge in multicore programs is that determinism lies in the eye of the beholder. If two executions of the same program with the same input produce outputs that are non-identical but semantically equivalent, should the program be considered deterministic or not? For example, consider a program that produces two different floating-point values in two executions with the same input. From the viewpoint of a strict definition of determinism, the program is unquestionably nondeterministic. From the viewpoint of a more relaxed definition in which all values within a certain error threshold are permissible as outputs, the program may well be considered to be deterministic. A similar situation arises for programs that produce (say) ordered linked lists as data structure representations of unordered sets. Two non-identical outputs may still be considered equivalent if they contain the same set of elements, albeit in different orders.
Given this range of interpretations for determinism, it isn’t obvious how assertions for determinism should be formulated. The approach taken in this paper is to extend the concepts of preconditions ("assume" clauses) and 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.
A key challenge in multicore programs is that determinism lies in the eye of the beholder.
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!
Join the Discussion (0)
Become a Member or Sign In to Post a Comment