Counterexample-guided abstraction refinement for symmetric concurrent programs
Counterexample-guided abstraction refinement for symmetric concurrent programs
复制标题
DOI：
10.1007/s10703-012-0155-3
复制
发表时间：
2012-04
影响因子：
0.8
通讯作者：
Alastair F. Donaldson;A. Kaiser;D. Kroening;Michael Tautschnig;T. Wahl
中科院分区：
文献类型：
--
作者：
Alastair F. Donaldson;A. Kaiser;D. Kroening;Michael Tautschnig;T. Wahl
谓词抽象和反例引导的抽象细化（CEGAR）使得能够对用主流编程语言编写的软件进行有限状态模型检查。这种技术组合已成功分析系统级顺序 C 代码。相比之下，几乎没有证据表明 CEGAR 在共享变量并发软件中取得了卓有成效的应用。我们将这种差距归因于缺乏允许对生成的多线程布尔程序进行可扩展分析的抽象策略。本文的目标是缩小这一差距。我们开发了非对称感知CEGAR技术：它考虑了由执行同一过程的许多线程组成的程序的复制结构，并生成一个布尔程序模板，其多线程执行完全近似于原始并发程序。现在可以通过利用对称性来吸收该模板的模型检查并行实例化过程中的状态爆炸。我们已经在工具 SymmPa 中实现了我们的方法，并在一系列同步程序上证明了其优于替代方法的性能。
Predicate abstraction and counterexample-guided abstraction refinement (CEGAR) have enabled finite-state model checking of software written in mainstream programming languages. This combination of techniques has been successful in analysing system-level sequentialCcode. In contrast, there is little evidence of fruitful applications of CEGAR to shared-variableconcurrentsoftware. We attribute this gap to the lack of abstraction strategies that permit a scalable analysis of the resulting multi-threaded Boolean programs. The goal of this paper is to close this gap. We have developed asymmetry-awareCEGAR technique: it takes into account the replicated structure of programs that consist of many threads executing the same procedure, and generates a Boolean program template whose multi-threaded execution soundly overapproximates the original concurrent program. State explosion during model checking parallel instantiations of this template can now be absorbed by exploiting symmetry. We have implemented our method in a tool,SymmPa, and demonstrate its superior performance over alternative approaches on a range of synchronisation programs.