POWER的上下文有界模型检验
Context-Bounded Model Checking for POWER
摘要：
基于Qadeer等人在2005年提出的用于检测并发程序（假定运行在经典SC模型下）中bug的上下文有界分析的工作，我们提出了一种针对POWER内存模型下运行的程序的欠近似可达性分析算法.为此，我们首先引入了一个新的上下文绑定概念，它适用于POWER下的计算推理，它概括了Atig等人在2011年为TSO内存模型定义的概念。然后，我们提供了一个多项式大小减少的上下文有界状态的可达性问题下POWER SC下相同的问题：给定一个输入并发程序P，我们的方法产生一个并发程序P'，这样，对于一个固定数量的上下文切换，运行P' SC下产生相同的一组可达状态下运行P POWER。生成的程序P'包含与P相同数量的进程，并且在相同的数据域上操作。通过利用标准的模型检查器CBMC，我们已经实现了一个原型工具，并将其应用于一组基准测试，表明我们的方法的可行性。
英文摘要：
We propose an under-approximate reachability analysis algorithm for programs running under the POWER memory model, in the spirit of the work on context-bounded analysis intitiated by Qadeer et al. in 2005 for detecting bugs in concurrent programs (supposed to be running under the classical SC model). To that end, we first introduce a new notion of context-bounding that is suitable for reasoning about computations under POWER, which generalizes the one defined by Atig et al. in 2011 for the TSO memory model. Then, we provide a polynomial size reduction of the context-bounded state reachability problem under POWER to the same problem under SC: Given an input concurrent program P, our method produces a concurrent program P' such that, for a fixed number of context switches, running P' under SC yields the same set of reachable states as running P under POWER. The generated program P' contains the same number of processes as P, and operates on the same data domain. By leveraging the standard model checker CBMC, we have implemented a prototype tool and applied it on a set of benchmarks, showing the feasibility of our approach.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
