Lazy TSO Reachability
Lazy TSO Reachability
复制标题
惰性 TSO 可达性
DOI：
10.1007/978-3-662-46675-9_18
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
R. Meyer
中科院分区：
文献类型：
--
作者：
A. Bouajjani;G. Călin;E. Derevenetc;R. Meyer
我们解决的问题，检查状态可达性的程序下运行的总存储顺序（TSO）。问题已被证明是可判定的，但成本是禁止的，即非原始递归。我们在这里建议放弃完整性。我们的贡献是一个新的算法TSO可达性：它使用标准的SC语义，并介绍了TSO语义懒，只在需要的地方。我们算法的核心是对感兴趣的程序进行迭代改进。如果程序的目标状态是SC可达的，我们就完成了。如果目标状态不是SC可达的，则这可能是由于SC欠近似TSO的事实。我们采用第二种算法，确定TSO计算是不可行的SC下，因此可能会导致新的状态。我们丰富的程序来模拟，SC下，这些TSO计算。总之，这产生了一个迭代的欠近似，我们证明了声音和完整的错误狩猎，即，一个半决策过程，在可达性为正的情况下停止。我们已经实现了该过程作为工具Trencher [1]的扩展，并将其与Apriax [2]和CBMC [14]模型检查器进行了比较。
We address the problem of checking state reachability for programs running under Total Store Order (TSO). The problem has been shown to be decidable but the cost is prohibitive, namely non-primitive recursive. We propose here to give up completeness. Our contribution is a new algorithm for TSO reachability: it uses the standard SC semantics and introduces the TSO semantics lazily and only where needed. At the heart of our algorithm is an iterative refinement of the program of interest. If the program’s goal state is SC-reachable, we are done. If the goal state is not SC-reachable, this may be due to the fact that SC underapproximates TSO. We employ a second algorithm that determines TSO computations which are infeasible under SC, and hence likely to lead to new states. We enrich the program to emulate, under SC, these TSO computations. Altogether, this yields an iterative under-approximation that we prove sound and complete for bug hunting, i.e., a semi-decision procedure halting for positive cases of reachability.We have implemented the procedure as an extension to the tool Trencher [1] and compared it to the Memorax [2] and CBMC [14] model checkers.
登录
查看更多内容
一种基于自动机的在宽松内存模型上验证程序的符号方法
DOI：
10.1007/978-3-642-16164-3_16
发表时间：
2010
期刊：
bioRxiv
影响因子：
--
作者：
A. Linden;P. Wolper
通讯作者：
P. Wolper
DOI：
10.1007/978-3-540-70545-1_12
发表时间：
2008-07
期刊：
--
影响因子：
--
作者：
S. Burckhardt;M. Musuvathi
通讯作者：
S. Burckhardt;M. Musuvathi
DOI：
10.1007/978-3-642-37036-6_28
发表时间：
2012-07
期刊：
--
影响因子：
--
作者：
J. Alglave;D. Kroening;Vincent Nimal;Michael Tautschnig
通讯作者：
J. Alglave;D. Kroening;Vincent Nimal;Michael Tautschnig
更好的 x86 内存模型：x86-TSO（扩展版本）
DOI：
--
发表时间：
2009
期刊：
影响因子：
--
作者：
Scott Owens;Susmit Sarkar;Peter Sewell
通讯作者：
Peter Sewell
对宽松记忆模型的顺序一致性进行健全且完整的监控
DOI：
--
发表时间：
2011
期刊：
International Conference on Tools and Algorithms for Construction and Analysis of Systems
影响因子：
--
作者：
Jacob Burnim;Koushik Sen;C. Stergiou
通讯作者：
C. Stergiou