Efficient Verification of Software with Replicated Components

Concurrency is a model of computation that allows many units of execution to coexist. It is ubiquitous in computer science today: user processes in a time-sharing operating system execute concurrently, as do worker threads in client-server environment. Parallel processing, once primarily of interest in high-performance computing, has emerged in recent years as a new way of increasing processing power, such as in multi-core concurrent
systems, even for the home personal computer.

Concurrency poses new challenges for the quality assurance of software, for two reasons. First, concurrent programs have the potential for forms of errors unknown in sequential computation, such as race conditions and mutual exclusion violations. Second, traditional reliability measures such as simulation and testing fail in the presence of concurrency, due to the difficulties of reproducing erroneous behavior. Model Checking is an automated technique to reliably establish the correctness of software, or to reveal the existence of errors in a reproducible manner. A program is represented by a finite-state model, which is exhaustively searched for violations of pre-specified properties. Exhaustive search, however, generally incurs a cost proportional to the number of model states that are reached during the search. This number is in turn worst-case exponential in the number of concurrent components. This state space explosion problem has been a major obstacle to the widespread use of model checking.

One avenue of our research is guided by the observation that concurrent ystems often consist of replicated components: instances of a single template, generically describing the behavior of each component. Concurrent systems of replicated components often exhibit a very regular - symmetric - structure: their behavior is invariant under interchanges of the components. This causes redundancy in the system model and in the (naive) exploration of the model's state space.

We propose to investigate the efficacy of symmetry reduction and parameterized verification to attack the state space explosion problem for software with replicated components. Both techniques have shown to be tremendously effective in principle, namely due to their potential of reducing the size of a symmetric system by an exponential factor, or of collapsing the verification problem for an infinite family of systems to one for a single system or a small finite family, respectively. The applicability of these techniques to concurrent software was hampered, however, by the apparent incapability of model checking to deal with integer variables over very large domains or even unbounded, dynamic data structures. The situation changed dramatically with the advent of automated abstraction-refinement techniques. Software is initially represented abstractly using coarse finite-state models, risking the possibility of incorrect - spurious - verification results. The new paradigm came with ways of detecting spuriousness, and of dealing with it by iteratively refining the abstract model until spurious behavior is removed.

To sum up, concurrent software exhibits two sources of complexity: large variable data domains and concurrency. Fortunately, these sources are orthogonal and can be attacked separately. This separation makes it possible to apply symmetry reduction and parameterized techniques to concurrent software, methods that target the concurrency aspect of state space explosion. The ultimate goal of the proposed work is to combine these methods with iterative abstraction refinement to obtain verification tools for concurrent software that can seriously curb state space explosion at all levels.