Efficient Verification of Software with Replicated Components

点击翻译按钮获取中文摘要

Concurrency is a model of computation that allows many units of executionto coexist. It is ubiquitous in computer science today: user processes in atime-sharing operating system execute concurrently, as do worker threads ina client-server environment. Parallel processing, once primarily ofinterest in high-performance computing, has emerged in recent years as anew way of increasing processing power, such as in multi-core concurrentsystems, even for the home personal computer.Concurrency poses new challenges for the quality assurance of software, fortwo reasons. First, concurrent programs have the potential for forms oferrors unknown in sequential computation, such as race conditions andmutual exclusion violations. Second, traditional reliability measures suchas simulation and testing fail in the presence of concurrency, due to thedifficulties of reproducing erroneous behavior. Model Checking is anautomated technique to reliably establish the correctness of software, orto reveal the existence of errors in a reproducible manner. A program isrepresented by a finite-state model, which is exhaustively searched forviolations of pre-specified properties.Exhaustive search, however, generally incurs a cost proportional to thenumber of model states that are reached during the search. This number isin turn worst-case exponential in the number of concurrent components. Thisstate space explosion problem has been a major obstacle to the widespreaduse of model checking.One avenue of our research is guided by the observation that concurrentsystems often consist of replicated components: instances of a singletemplate, generically describing the behavior of each component. Concurrentsystems of replicated components often exhibit a veryregular---symmetric---structure: their behavior is invariant underinterchanges of the components. This causes redundancy in the system modeland in the (naive) exploration of the model's state space.We propose to investigate the efficacy of symmetry reduction andparameterized verification to attack the state space explosion problem forsoftware with replicated components. Both techniques have shown to betremendously effective in principle, namely due to their potential ofreducing the size of a symmetric system by an exponential factor, or ofcollapsing the verification problem for an infinite family of systems toone 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 withinteger variables over very large domains or even unbounded, dynamic datastructures. The situation changed dramatically with the advent of automatedabstraction-refinement techniques. Software is initially representedabstractly using coarse finite-state models, risking the possibility ofincorrect---spurious---verification results. The new paradigm came withways of detecting spuriousness, and of dealing with it by iterativelyrefining the abstract model until spurious behavior is removed.To sum up, concurrent software exhibits two sources of complexity: largevariable data domains and concurrency. Fortunately, these sources areorthogonal and can be attacked separately. This separation makes itpossible to apply symmetry reduction and parameterized techniques toconcurrent software, methods that target the concurrency aspect of statespace explosion. The ultimate goal of the proposed work is to combine thesemethods with iterative abstraction refinement to obtain verification toolsfor concurrent software that can seriously curb state space explosion atall levels.