A variety of approaches for debugging non-deterministic concurrent software have been proposed. Most are based on either dynamic trace collection or static analysis. We argue that integration of static and dynamic analysis techniques enables the user to better understand the state space of a faulty concurrent program, and this will aid debugging. This dissertation presents our work in developing a debugging methodology with two components; a framework for representing the state space of concurrent programs, and a set of static and dynamic techniques for exploring this state space. Our focus is currently on Ada programs, but the approach is applicable to any language using the rendezvous model of concurrency.
We provide a visualization of the state space using the Task Interaction Concurrency Graph (TICG). The TICG is a data structure normally built during static concurrency analysis. We capture traces describing the concurrency related events that occur during a particular execution, then build a TICG to represent this execution. The user can then explore this TICG, and expand it further using static concurrency analysis to determine what other executions the could have occurred. We also provide a means of limiting the portion of the state space generated, and of limiting the analysis to a subset of the tasks that comprise the system under test.
This synergistic combination of static and dynamic techniques allows analysis of larger and more complex systems than is possible with conventional static concurrency, yet retains many of the benefits of automation and guidance provided by the formal models used in static concurrency analysis.