SADCPU (Static concurrency analysis Aiding Dynamic Concurrent Program Understanding)

SADCPU provides a framework to help the programmer understand the complex dynamic behavior of concurrent programs. It does this by creating a model of the possible behaviors of a concurrent program from the static source text of a program, and relating which of these behaviors occurred during a particular observed execution. It also gives insight into other, similar executions which could have occurred given different non-deterministic scheduling decisions, or slightly different input values.

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.

SADCPU Source code:

Feel free to download the source code for SADCPU (712k). If you want to compile and run the system you should contact me, since getting it running is a bit tricky and dependent on the platform, as well as the versions of several other pieces of software.