Reachability testing of concurrent programs

One approach to testing concurrent programs, called reachability testing, generates synchronization sequences automatically and on-the-fly, without constructing any static models. In this paper, we present a general execution model for concurrent programs that allows reachability testing to be applied to several commonly used synchronization constructs. We also present a new method for performing reachability testing. This new method guarantees that every partially ordered synchronization sequence will be exercised exactly once without having to save any sequences that have already been exercised. We describe a prototype reachability testing tool called RichTest and report some empirical results, including a comparison between RichTest and a partial order reduction-based tool called VeriSoft. RichTest performed significantly better for the programs in our study

1 Introduction

A concurrent program contains two or more threads that execute concurrently and work together to perform some task. Using multiple threads, a.k.a. multithreading, can increase computational efficiency. For instance, while one thread is waiting for user input, another thread can perform computational tasks in the background. In addition, many problem domains are, by nature, concurrent and can be solved more naturally by creating multiple threads. As an example, a Web server typically creates separate threads to service incoming client requests. Some languages, such as Java and Ada, provide built-in support for concurrent programming. The POSIX Pthreads library can be used to write concurrent programs in other languages such as C and C++.