• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>International Symposium on Static Analysis >Effect Summaries for Thread-Modular Analysis Sound Analysis Despite an Unsound Heuristic
【24h】

Effect Summaries for Thread-Modular Analysis Sound Analysis Despite an Unsound Heuristic

机译：尽管声音听起来不合理，但线程模块分析声音分析的效果摘要

获取原文
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

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.
机译：我们提出了一种新颖的猜测和检查原理，以提高无锁数据结构的线程模块化验证的效率。我们建立在一种启发式方法上，该方法通过在代码中搜索无锁数据结构中常见的复制检查程序惯用法实例来猜测程序的无状态效果摘要的候选项。这些候选摘要用于计算线性时间内线程之间的干扰。由于候选摘要不必是声音效果摘要，因此我们展示了如何完全自动检查候选摘要的精度是否足够。因此，尽管依赖于不健全的启发式方法，我们仍可以执行声音验证。我们已经实施了我们的方法，发现它比现有方法快两个数量级。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号