Automated Verification of Concurrent Recursive Programs

Motivation

Concurrent programs are (more and more) present at different levels of computer systems, going from distributed applications for large networks, to basic software running on multi-core processors, while passing by multi-tasking operating systems and multi-threaded programs. The design and development of concurrent systems present many challenges due to the complexity of their behavior, which results from the interaction between their components. It is therefore crucial to develop formal methods to automatically verify their correctness with respect to some specification.

From an abstract point of view, it is possible to reason about concurrent programs as networks of sequential systems, where each system has its own local memory and can communicate with the others by different means. Depending on the considered class of programs, communication mechanisms include: shared memory or message passing through channels of various types. The networks can be either static (i.e., have a fixed number of components (or processes)), or dynamic (i.e., components can be created during its execution).

Another dimension of complexity is the program variables which can range over an infinite domain. But even if we assume the variables domain to be finite (which can be obtained after applying, for instance, the predicate abstraction techniques) the complexity due to concurrency and interaction between the processes remains a highly nontrivial problem. In this project, we focus on the aspects related to the concurrency and we leave aside the treatment of data.

In this work, we are interested in verifying concurrent programs where each process corresponds to a sequential program with (recursive) procedure calls. It is well admitted that pushdown systems are adequate models for such kind of processes, and therefore, it is natural to model concurrent programs as networks of pushdown systems. The difficulty in analyzing such networks comes from the interaction between recursion and concurrency which makes almost all verification problems undecidable in general.

To overcome this difficulty, two complementary approaches can be adopted for the analysis of this class of programs. The first approach consists in defining techniques that over-approximate the behavior of a program. This approach can be used to show that a program is correct with respect to a given specification. The second approach consists in defining techniques based on the computations of under-approximations of all behaviors. These techniques are useful to detect bugs in programs but they can not ensure the correctness of a program.

Long Term Goal

The goal of the project is developing scalable under and over approximation techniques for concurrent concurrent programs (with reasonable complexity), and complete for some particular sub-classes. A long-term challenge is the development of tools for the automatic verification of concurrent recursive programs.

Achievements

In [Atig, FSTTCS 2010], we address the verification problem of ordered multi-pushdown systems: A multi-stack extension of pushdown systems that comes with a constraint on stack operations such that a pop can only be performed on the first non-empty stack. First, we show that for an ordered multi-pushdown system the set of all predecessors of a regular set of configurations is an effectively constructible regular set. Then, we exploit this result to solve the global model checking which consists in computing the set of all configurations of an ordered multi-pushdown system that satisfy a given w-regular property (expressible in linear-time temporal logics or the linear-time mu-calculus). As an immediate consequence of this result, we obtain an 2ETIME upper bound for the model checking problem of w-regular properties for ordered multi-pushdown systems (matching its lower-bound).

In [Atig, CONCUR 2010], we investigate the issue of reducing the verification problem of multi-stack machines to the one for single-stack machines. We extend this view to both bounded-phase visibly pushdown automata (BVMPA) and ordered multi-pushdown automata (OMPA) by showing that each of their emptiness problems can be reduced to the one for a class of single-stack machines called effective generalized pushdown automata (EGPA). Our reductions from OMPA and BVMPA to EGPA, together with the reachability analysis procedure for EGPA, allow to provide conceptually simple algorithms for checking the emptiness problem for each of these models, and to significantly simplify the proofs for their 2ETIME upper bounds (matching their lower-bounds).

In [Atig et al., TCS 2010], we address the verification problem of networks of communicating pushdown systems. Processes in such networks can read the control state of the other processes according to a given communication structure (specifying the observability rights between processes). We consider networks where the communication structure can change dynamically during the execution according to a phase graph. The reachability problem for these dynamic networks being undecidable in general, we define a subclass for which it becomes decidable. Then, we consider reachability when the switches in the communication structures are bounded. We show that this problem is undecidable even for one switch. Then, we define a natural class of models for which this problem is decidable. This class can be used in the definition of an efficient semi-decision procedure for the analysis of the general model of dynamic networks. Our techniques allowed to find bugs in two versions of a Windows NT Bluetooth driver.

In [Stenman, M.Sc. Thesis], we under-approximate the shuffle of context-free languages corresponding to program threads. We are trying to complement context-bounded model checking with a technique that may detect errors regardless of the number of context-switches. Instead of bounding the number of context-switches, we bound the granularity of the approximation of interleaving runs. The idea is to take a program consisting of several threads and generate a formal grammar which produces an underapproximation of all possible interleaving runs of the threads. We implemented a prototype tool which detects errors in some example programs, including a Windows NT Bluetooth driver.

Current Work

We are developing a prototype for the reachability analysis of concurrent recursive pushdown automata. This prototype is based on an efficient approximation of the language obtained by the shuffle of two context-free languages by a context-free language.

We are also working on the issue of reducing the verification problem of concurrent programs to the corresponding one for sequential programs under some conditions on the explored behaviors. The idea is to propose code-to-code translations that take as input a concurrent program P and produces a sequential program P' such that, running P' yields the same set of reachable (shared) states as running P under some conditions. For instance, elegant (and practically efficient) algorithms for bounded-context switch analysis of concurrent recursive programs have been recently defined based on reductions to the reachability problem for sequential recursive programs.

On the other side, we are working on game and synthesis problems for various sub-classes of concurrent pushdown systems.

Approach

We are using automata for modeling concurrent programs. Different types of automata naturally correspond to different types of programs, and provide an efficient symbolic representation.

We are also investigating the use of methods based on SMT and SAT solvers. We can extract assertions (i.e. formulas in some logic) from programs (using e.g. summarization) and check these with tools specialized on checking logical formulas.

Publications

Staff

Senior: Parosh Abdulla (Contact), Mohamed Faouzi Atig
Ph.D. students: Jari Stenman