Efficient Verification of Software with Replicated Components

并发是一种允许多个执行单元共存的计算模型。它在当今计算机科学中随处可见：atime共享操作系统中的用户进程并发执行，客户端-服务器环境中的工作线程也是如此。并行处理曾经主要用于高性能计算，近年来作为一种提高处理能力的新方法出现，例如在多核并发系统中，甚至对于家用个人计算机。并发对软件的质量保证提出了新的挑战，原因有两个。首先，并发程序有可能出现顺序计算中未知的错误形式，如竞争条件和互斥违规。其次，由于复制错误行为的困难，传统的可靠性测量，如模拟和测试，在并发存在的情况下失败。模型检查是一种自动技术，用于可靠地确定软件的正确性，或以可重现的方式揭示错误的存在。一个程序由一个有限状态模型表示，它被穷尽地搜索是否违反了预先指定的属性。然而，Exhaustive搜索通常会产生与搜索过程中达到的模型状态数量成正比的成本。在最坏的情况下，这个数字是并发组件数量的指数。这种状态空间爆炸问题一直是模型检验广泛应用的主要障碍。我们的一种研究方法是观察到并发系统通常由重复的组件组成：单个模板的实例，一般地描述每个组件的行为。复制组件的并发系统通常表现出非常规则的-对称--结构：它们的行为在组件互换下是不变的。这导致了系统模型中的冗余和对模型状态空间的(幼稚)探索。我们建议研究对称性约简和参数验证对解决具有复制组件的软件的状态空间爆炸问题的有效性。这两种技术在原则上都被证明是非常有效的，这是因为它们可能将对称系统的大小减少一个指数倍，或者将无限系统的验证问题分别压缩为单个系统或一个小有限族的验证问题。然而，由于模型检测显然不能处理非常大的域甚至是无界的动态数据结构上的整数变量，这些技术在并发软件中的适用性受到了阻碍。随着自动化抽象-细化技术的出现，情况发生了戏剧性的变化。软件最初使用粗略的有限状态模型抽象地表示，冒着错误-虚假-验证结果的可能性。新的范式包括检测伪造性的方法，以及通过迭代地精炼抽象模型直到去除伪造性行为来处理它的方法。幸运的是，这些信源是正交的，可以单独攻击。这种分离使得将对称性缩减和参数化技术应用于并发软件成为可能，这些方法针对状态空间爆炸的并发方面。该工作的最终目标是将这些方法与迭代抽象求精相结合，为并发软件获得能够在所有级别上有效抑制状态空间爆炸的验证工具。

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.