论文标题
低级C代码中的静态僵局检测
Static Deadlock Detection in Low-Level C Code
论文作者
论文摘要
我们提出了一种新颖的可扩展僵局分析仪L2D2，能够处理低级非结构化锁操作的C代码。 L2D2沿程序的呼叫树运行，从其叶子开始，并仅分析每个功能一次，而无需任何呼叫上下文。 L2D2构建函数摘要记录有关锁定的信息，这些信息被假定或已知在输入，内部和功能出口处被锁定或解锁，以及锁定依赖性，并报告有关检测到锁定依赖锁定的循环时可能发生的僵局的警告。我们实施了L2D2作为Facebook/Meta推断框架的插件，并报告了大量C的实验结果以及C ++代码，以说明L2D2的有效性和效率。
We present a novel scalable deadlock analyser L2D2 capable of handling C code with low-level unstructured lock manipulation. L2D2 runs along the call tree of a program, starting from its leaves, and analyses each function just once, without any knowledge of the call context. L2D2 builds function summaries recording information about locks that are assumed or known to be locked or unlocked at the entry, inside, and at the exit of functions, together with lock dependencies, and reports warnings about possible deadlocks when cycles in the lock dependencies are detected. We implemented L2D2 as a plugin of the Facebook/Meta Infer framework and report results of experiments on a large body of C as well as C++ code illustrating the effectiveness and efficiency of L2D2.
