Reachability testing of semaphore-based programs

Concurrent programming is becoming more important in modern software development. However, concurrent programs exhibit non-deterministic behavior, which makes them difficult to test. In this paper, we describe how to apply reachability testing to semaphore-based multithreaded programs, i.e., programs that use semaphores to synchronize operations on shared data. A novel aspect of reachability testing is that it derives test sequences on-the-fly, avoiding the construction of any static models. Also, our reachability testing algorithms deal with partial orders directly, avoiding the test sequence explosion problem that occurs when independent events are interleaved. We describe a prototype tool called RichTest and report some preliminary results