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.