Automated Systematic Testing Methods for Multithreaded Programs
Kari Kähkönen · Aaltodoc (Aalto University) · 2015
This thesis considers the problem of how the testing of multithreaded programs can be automated.One of the reasons multithreaded programs are difficult to test is that their behavior does not only depend on input values but also on how the executions of threads are interleaved. Typically this results in a number of possible executions through a multithreaded program that is so large that covering them all, even with the help of a computer, is infeasible. Fortunately it is often not necessary to test all combinations of input values and interleavings as many of them cause the program to behave in a similar way. This opens up the research question of how to automatically cover interesting properties of the program under test while trying to keep the number of test executions small. This work studies how two different approaches, dynamic symbolic execution and net unfoldings, can be combined to automatically test multithreaded programs. Dynamic symbolic execution is a popular approach to automatically generate tests for sequential programs. Net unfoldings, on the other hand, can be used in verification of concurrent systems. The main contributions of this thesis fall under three categories. First, two net unfolding based approaches to systematically cover the local reachable states of threads are presented. Second, the thesis describes how global reachability properties, such as deadlock freedom, can be checked from an unfolding of a program. Third, a lightweight approach to capture abstract states of a multithreaded programs is presented. The method can be used to stop a test execution if it reaches an already covered abstract state. To evaluate the new approaches, they are compared against an existing partial order reduction based testing algorithm. This is done by applying the algorithms to a number of multithreaded programs. Based on the results, the new algorithms are competitive against more traditional partial order reduction based methods and can in some cases outperform existing approaches by a considerable margin.