Effect Summaries for Thread-Modular Analysis
Effect Summaries for Thread-Modular Analysis
复制标题
线程模块化分析的效果摘要
DOI：
10.1007/978-3-319-66706-5_9
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
S. Wolff
中科院分区：
文献类型：
--
作者：
L. Holík;R. Meyer;T. Vojnar;S. Wolff
我们提出了一种新的猜测和检查的原则，以提高无锁数据结构的线程模块验证的效率。我们建立在一个启发式的猜测候选人的无状态效果摘要的程序，通过搜索代码的实例的复制和检查编程习惯用法常见的无锁数据结构。这些候选摘要用于计算线性时间内线程间的干涉。由于候选摘要不需要是音效摘要，我们展示了如何完全自动地检查候选摘要的精度是否足够。因此，我们可以执行健全的验证，尽管依赖于不健全的启发式。我们已经实施了我们的方法，发现它比现有的方法快了两个数量级。
We propose a novel guess-and-check principle to increase the efficiency of thread-modular verification of lock-free data structures. We build on a heuristic that guesses candidates for stateless effect summaries of programs by searching the code for instances of a copy-and-check programming idiom common in lock-free data structures. These candidate summaries are used to compute the interference among threads in linear time. Since a candidate summary need not be a sound effect summary, we show how to fully automatically check whether the precision of candidate summaries is sufficient. We can thus perform sound verification despite relying on an unsound heuristic. We have implemented our approach and found it up to two orders of magnitude faster than existing ones.
登录
查看更多内容
线程模块化验证是笛卡尔抽象解释
影响因子：
0.8
作者：
A. Malkis;A. Podelski;A. Rybalchenko
通讯作者：
A. Rybalchenko
使用关系干扰抽象对并发程序进行精确的线程模块化抽象解释
DOI：
10.1007/978-3-319-52234-0_21
发表时间：
2017
期刊：
2014 Formal Methods in Computer-Aided Design (FMCAD)
影响因子：
--
作者：
Raphaël Monat;A. Miné
通讯作者：
A. Miné
DOI：
--
发表时间：
2013
期刊：
European Symposium on Programming
影响因子：
--
作者：
Alexey Gotsman;N. Rinetzky;Hongseok Yang
通讯作者：
Hongseok Yang
使用细化微积分技术来证明线性化能力
影响因子：
1
作者：
B. Jonsson
通讯作者：
B. Jonsson
用于线程相关性分析的抽象变压器
DOI：
10.1007/978-3-642-10672-9_5
发表时间：
2009
期刊：
The international journal of biochemistry & cell biology
影响因子：
--
作者：
M. Segalov;T. Lev;R. Manevich;Ramalingam Ganesan;M. Sagiv
通讯作者：
M. Sagiv