低级 C 代码中的静态死锁检测
软件工程
2022-07-06 v1 分布式、并行与集群计算
编程语言
摘要
我们提出了一种新颖的可扩展死锁分析器 L2D2，能够处理具有低级非结构化锁操作的 C 代码。L2D2 沿程序的调用树自叶子节点开始运行，对每个函数仅分析一次，且无需任何调用上下文信息。L2D2 构建函数摘要，记录函数在入口、内部及出口处假定或已知被锁定或解锁的锁信息，以及锁依赖关系，并在检测到锁依赖中存在环时报告可能的死锁警告。我们将 L2D2 实现为 Facebook/Meta Infer 框架的一个插件，并报告在大量 C 及 C++ 代码上的实验结果，说明了 L2D2 的有效性与高效性。
引用
@article{arxiv.2207.01948,
title = {Static Deadlock Detection in Low-Level C Code},
author = {Dominik Harmim and Vladimír Marcin and Lucie Svobodová and Tomáš Vojnar},
journal= {arXiv preprint arXiv:2207.01948},
year = {2022}
}
备注
A pre-print submitted for publication in the post-proceedings of the EUROCAST'22 conference