Interprocedural Analysis and the Verification of Concurrent Programs

Akash Lal
University of Wisconsin

In the modern world, not only is software getting larger and more complex, it is also becoming pervasive in our daily lives. On the one hand, the advent of multi-core processors is pushing software towards becoming more concurrent, making it more complex. On the other hand, software is everywhere, inside nuclear reactors, space shuttles, cars, traffic signals, cell phones, etc. To meet this demand for software, we need to invest in automated program-verification techniques, which ensure that software will always behave as intended.

The problem of program verification is undecidable. A verification technique can only gain a limited amount of knowledge about a program's behavior by reasoning about certain aspects of the program. This dissertation addresses program verification by considering two important features of programs: (i) procedures (and procedure calls) and (ii) concurrency.

Interprocedural Analysis: An analysis that can precisely handle the procedural aspect of programs is called an interprocedural analysis. Procedures are an important feature of most programming languages because they allow for modular design of programs: each procedure is meant to perform a task, and they can be put together to implement more complex functionality. Because procedures serve as a natural abstraction mechanism for developers to organize their programs, an interprocedural analysis can leverage them to enable verification of a larger and more complex programs.

There is a long history of work on interprocedural analysis, including several frameworks that support a variety of different program abstractions, and provide algorithms for analyzing them. The advantage of having a framework is that any program abstraction that fits the framework can make use of the algorithms for the framework. One such framework, called Weighted Pushdown Systems (WPDSs), was the subject of the research reported on in this dissertation.

The dissertation makes several contributions to interprocedural analyses that are based on WPDSs:

We define the Extended WPDS (EWPDS) model, which removes a crucial limitation of WPDSs by providing a convenient abstraction mechanism for local variables of a procedure. Using EWPDSs, it is possible to model a program's behavior more precisely than with WPDSs. In our work, we used EWPDSs for checking properties of Boolean programs; computing affine relations in x86 programs; building debugging tools; computing alias pairs in programs with single-level pointers; and for checking properties of concurrent programs (where EWPDSs are used to model individual threads).

We use graph-theoretic algorithms to speed up the analysis algorithms for WPDSs and EWPDSs. This results in immediate speedup in all of the applications based on these models without requiring any tuning for a particular application. The speedups ranged from 1.8x to 3.6x.

We show how to answer more expressive queries on EWPDSs, such as computing the set of all error traces in the model, called an error projection. This enables faster verification.

Concurrency: The advent of multi-core processors is pushing software to become more concurrent. Concurrent programs are not only difficult to write, but are also difficult to analyze and verify. One reason is that the interprocedural analysis of concurrent programs is undecidable, even when all of the other aspects of a programs (like the program heap, non-scalar variables, pointers, etc.) are abstracted away. As a result, most verification tools do not mix interprocedural analysis with concurrency, i.e., tools that analyze concurrent programs give up on precise handling of procedures. This is unfortunate because precise handling of procedures has proven to be very useful for the analysis of sequential programs.

The contribution of our work is to give techniques for interprocedural analysis for concurrent programs. We show that one does not have to design new algorithms for concurrent programs; instead, it is possible to automatically extend most interprocedural analysis techniques for sequential programs to perform interprocedural analysis of concurrent programs.

As mentioned earlier, interprocedural analysis of concurrent programs is undecidable. We sidestep the undecidability by placing a bound on the number of context switches, i.e., we bound the number of times control is transferred from one thread to another. We call the analysis of concurrent programs under a bound on the number of context switches context-bounded analysis (CBA).

CBA is an interesting avenue of research that has attracted a lot of attention recently because empirical evidence suggests that many concurrency-related bugs can be found in a few context switches. Moreover, CBA was shown to be decidable for finite-data abstractions.

The dissertation makes two important contributions to interprocedural analysis of concurrent programs:

We show that if each thread is modeled using a WPDS then CBA is decidable, and also give an algorithm for performing CBA. This represents the first step towards providing a general model for concurrent programs that can be used to perform interprocedural analysis.
We show that, given a concurrent program P and a context bound K, one can create a sequential program P_K such that the analysis of P_K is sufficient for CBA of P under the bound K. This reduction is a source-to-source transformation, and requires no assumptions nor extra work on the part of the user, except for the identification of thread-local data. We implemented this technique to create the first known implementation of CBA. Using this tool, we conducted a study on concurrent Linux drivers to show that most bugs could not only be found in a few context switches, but, compared to previous approaches, they could be found must faster using our approach.

(Click here to access the thesis: PDF.)