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 et al., DLT 2013], we propose a formal model for a subclass of ordered multi-pushdown systems, called Adjacent Ordered Multi-PushDown Systems, where values may be pushed only on the lowest non-empty stack or one of its two neighbours. We describe Exptime decision procedures for reachability and LTL model-checking and establish matching lower bounds. We demonstrate the utility of this model as an algorithmic tool via optimal reductions from other models.
In [Atig et al., ATVA 2012], We address the model checking problem of omega-regular linear-time properties for shared memory concurrent programs modeled as multi-pushdown systems. We consider here boolean programs with a finite number of threads and recursive procedures. It is well-known that the model checking problem is undecidable for this class of programs. In this paper, we investigate the decidability and the complexity of this problem under the assumption of scope-boundedness. A computation is scope-bounded if each pair of call and return events of a procedure executed by some thread must be separated by a bounded number of context-switches of that thread. The concept of scope-bounding generalizes the one of context-bounding since it allows an unbounded number of context switches. Moreover, while context-bounding is adequate for reasoning about safety properties, scope-bounding is more suitable for reasoning about liveness properties that must be checked over infinite computations. It has been shown in that the reachability problem for multi-pushdown systems under scope-bounding is PSPACE-complete. We prove in this paper that model-checking linear-time properties under scope-bounding is also decidable and is EXPTIME-complete.
In [Atig et al., FMCAD 2012], we address the verification problem for concurrent programs modeled as multi-pushdown systems (MPDS). In general, MPDS are Turing powerful and hence come along with undecidability of all basic decision problems. In this work, we propose the class of bounded-budget MPDS where we restrict them in the sense that each stack can perform an unbounded number of context switches if its size is below a given bound, and is restricted to a finite number of context switches when its size is above that bound. We show that the reachability problem for this subclass is PSPACE-complete. Furthermore, we propose a code-to-code translation that inputs a concurrent program P and produces a sequential program P' such that running P under the bounded-budget restriction yields the same set of reachable states as running P'. By leveraging standard sequential analysis tools, we have implemented a prototype tool and applied it on a set of benchmarks, showing the feasibility of our translation.
In [Atig et al., CAV 2012], we develop compositional analysis algorithms for discovering fair non-terminating executions in multithreaded programs. In particular, our analysis finds fair and ultimately-periodic executions-i.e., those that ultimately repeat the same sequence of actions indefinitely with each enabled thread participating. Further, we limit the number of context-switches each thread is allowed along any repeating sequence of actions; one expects that this number is usually small for bugs in practice. Bounding context-switches leads to a compositional analysis in which each thread is considered separately, in isolation. We implement our analysis by a systematic code-to-code translation from multithreaded programs to sequential programs, such that one requires a safety analysis of the latter to find liveness bugs in the former. Then by using standard sequential analysis tools, we are able to discover fair non-terminating executions in multithreaded programs.
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, Mohamed Faouzi Atig
Ph.D. students: Jari Stenman, Othmane Rezine