用于线程模块化分析的效应摘要
编程语言
2017-05-11 v1
摘要
我们提出一种新颖的猜测-检查原则，以提高无锁数据结构线程模块化验证的效率。我们基于一种启发式方法，该启发式通过搜索代码中无锁数据结构中常见的复制-检查编程惯用法实例来猜测程序的无状态效应摘要候选。这些候选摘要用于线性时间计算线程间干扰。由于候选摘要不必是可靠效应摘要，我们展示如何全自动检查候选摘要的精度是否足够。因此我们尽管依赖不可靠启发式，仍能执行可靠验证。我们已实现我们的方法，并发现其比现有方法快达两个数量级。
引用
@article{arxiv.1705.03701,
title = {Effect Summaries for Thread-Modular Analysis},
author = {Lukáš Holík and Roland Meyer and Tomáš Vojnar and Sebastian Wolff},
journal= {arXiv preprint arXiv:1705.03701},
year = {2017}
}