首页> 外文会议>International Haifa Verification Conference; 20051113-16; Haifa(IL) >Detecting Potential Deadlocks with Static Analysis and Run-Time Monitoring
【24h】

Detecting Potential Deadlocks with Static Analysis and Run-Time Monitoring

机译:通过静态分析和运行时监视来检测潜在的死锁

获取原文
获取原文并翻译 | 示例

摘要

Concurrent programs are notorious for containing errors that are difficult to reproduce and diagnose. A common kind of concurrency error is deadlock, which occurs when a set of threads is blocked each trying to acquire a lock held by another thread in that set. Static and dynamic (run-time) analysis techniques exist to detect deadlocks. Havelund's GoodLock algorithm detects potential deadlocks at runtime. However, it detects only potential deadlocks involving exactly two threads. This paper presents a generalized version of the GoodLock algorithm that detects potential deadlocks involving any number of threads. Run-time checking may miss errors in unexecuted code. On the positive side, run-time checking generally produces fewer false alarms than static analysis. This paper explores the use of static analysis to automatically reduce the overhead of run-time checking. We extend our type system, Extended Parameterized Atomic Java (EPAJ), which ensures absence of races and atomicity violations, with Boyapati et al.'s deadlock types. We give an algorithm that infers deadlock types for a given program and an algorithm that determines, based on the result of type inference, which run-time checks can safely be omitted. The new type system, called Deadlock-Free EPAJ (DEPAJ), has the added benefit of giving stronger atomicity guarantees than previous atomicity type systems.
机译:并发程序因包含难以重现和诊断的错误而臭名昭著。常见的并发错误是死锁,死锁发生在一组线程被阻塞时,每个线程都试图获取该组中另一个线程持有的锁。存在静态和动态(运行时)分析技术来检测死锁。 Havelund的GoodLock算法在运行时检测到潜在的死锁。但是,它仅检测到涉及两个线程的潜在死锁。本文介绍了GoodLock算法的通用版本,该版本可检测涉及任何数量线程的潜在死锁。运行时检查可能会丢失未执行代码中的错误。从积极的方面来说,运行时检查通常会比静态分析产生更少的错误警报。本文探索了使用静态分析来自动减少运行时检查的开销的方法。我们扩展了类型系统,即扩展参数化原子Java(EPAJ),该系统使用Boyapati等人的死锁类型来确保不存在种族和原子性违规。我们提供了一种推断给定程序的死锁类型的算法,以及一种基于类型推断的结果确定可以安全地省略哪些运行时检查的算法。这种新型系统称为无死锁EPAJ(DEPAJ),具有比以前的原子性类型系统更强的原子性保证的优点。

著录项

相似文献

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

客服邮箱:kefu@zhangqiaokeyan.com

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

  • 服务号