| 摘要: |
| 死锁是并行程序常见的缺陷之一，动态死锁分析方法根据程序运行轨迹构建锁图、分段图等模型来检测死锁.然而，锁图及其现有的各种变型无法区分同一循环中锁授权语句的多次执行，扩展锁图中记录的锁集无法捕捉线程曾经持有而又随后释放的锁信息，分段图无法刻画锁的获取和释放操作与线程启动操作耦合而导致的段间依赖关系.上述问题导致了多种死锁的误报.为解决上述问题，对已有的锁图和分段图模型进行改进，在锁图基础上扩充语句的执行时序信息，在分段图的基础上扩充锁的获取和释放信息，对段进行更细粒度的划分以建模锁对象导致的段间依赖关系；最终，在上述锁增广分段图与时序增广锁图的基础上，提出一种新的死锁检测方法.所提方法能够有效消除前述各种误报，从而提高死锁检测的准确率.文中开发相应的原型系统，并结合多个程序实例对所提方法的有效性进行评估验证. |
| 关键词: 程序验证 死锁检测 锁图 分段图 动态死锁分析 |
| DOI：10.13328/j.cnki.jos.006244 |
| 分类号: |
| 基金项目:国家自然科学基金（61602279，61472229）；国家重点研发计划（2016YFC0801406）；山东省泰山学者工程专项基金（ts20190936）；山东省高等学校青创科技支持计划（2019KJN024）；山东省自然科学基金智慧计算联合基金（ZL2019LZh001）；山东省博士后创新专项基金（201603056）；国家海洋局海洋遥测工程技术研究中心开放基金（2018002）；山东科技大学领军人才与优秀科研创新团队项目（2015TDJH102） |
|
| Deadlock Detection of Multithreaded Programs Based on Lock-augmented Segmentation Graph |
|
LU Fa-Ming1, ZHENG Jia-Jing1, BAO Yun-Xia2, ZENG Qing-Tian1, DUAN Hua2, WANG Xiao-Yu1
|
|
1.College of Computer Science and Engineering, Shandong University of Science and Technology, Qingdao 266590, China;2.College of Mathematics and Systems Science, Shandong University of Science and Technology, Qingdao 266590, China
|
| Abstract: |
| Deadlocks are a common defect of parallel programs. To detect deadlocks, dynamic deadlock analysis methods build models such as lock graphs and segment graphs according to program running traces. However, a lock graph and its existing variants cannot distinguish different executions of one lock acquisition statement in a loop structure. The lock set used in extended lock graphs cannot capture those locks which were once held and then released. A segmentation graph cannot model the inter-segment dependencies caused by the coupling of lock release/acquisition operation and thread start operation. The above problems have led to a variety of false positives. To address this issue, existing lock graph and segment graph models are improved. Specifically, a lock graph is extended with statement execution order information. A segmentation graph is expanded with lock acquisition and release information. Furthermore, segments in a segmentation graph are more finely divided in the improved model to capture the inter-segment dependencies caused by lock objects. Eventually, based on the improved models, a new deadlock detection method is proposed. It can eliminate the aforementioned false alarms effectively and improve deadlock detection accuracy. A corresponding prototype system is developed for experimental evaluation. The validity of the proposed method is verified through experiments. |
| Key words: program verification deadlock detection lock graph segmentation graph dynamic deadlock analysis |
