Lightweight and modular resource leak verification
Lightweight and modular resource leak verification
复制标题
DOI：
10.1145/3468264.3468576
复制
发表时间：
2021-08
期刊：
影响因子：
--
通讯作者：
Martin Kellogg;Narges Shadab;Manu Sridharan;Michael D. Ernst
中科院分区：
文献类型：
--
作者：
Martin Kellogg;Narges Shadab;Manu Sridharan;Michael D. Ernst
当程序分配资源（例如套接字或文件句柄）时，会发生资源泄漏，但无法对其进行处理。资源泄漏会导致资源饥饿，放缓和崩溃。以前的防止资源泄漏的技术是不合适的，不精确的，不适用于现有代码，缓慢或组合这些。资源泄漏的静态检测需要检查在相关对象变得无法到达之前，请始终调用分配方法。我们的关键见解是，泄漏检测可以简化为累积问题，一类典型的问题可以通过声音和模块化检查，而无需进行重量级，全程的别名分析。可以通过计算有针对性的别名信息来提高积累分析的精度，并使用三种这样的新技术增强了基线检查器：轻量级所有权转移系统；专门的资源别名分析；以及在更新非最终资源字段时创建新义务的系统。我们的方法占据了设计空间的独特切片：声音是合理的，并且运行速度相对较快（花费了最先进的方法花费数小时来分析的程序）。我们在称为资源泄漏检查器的开源工具中实现了Java的技术。资源泄漏检查器揭示了49个真正的资源泄漏在广泛部署的软件中。它的缩放良好，具有可管理的误报率（与Eclipse IDE内置的高信心资源泄漏分析相当），并且仅对开发人员施加一个小的注释负担（1/1500 LOC）。
A resource leak occurs when a program allocates a resource, such as a socket or file handle, but fails to deallocate it. Resource leaks cause resource starvation, slowdowns, and crashes. Previous techniques to prevent resource leaks are either unsound, imprecise, inapplicable to existing code, slow, or a combination of these. Static detection of resource leaks requires checking that de-allocation methods are always invoked on relevant objects before they become unreachable. Our key insight is that leak detection can be reduced to an accumulation problem, a class of typestate problems amenable to sound and modular checking without the need for a heavyweight, whole-program alias analysis. The precision of an accumulation analysis can be improved by computing targeted aliasing information, and we augmented our baseline checker with three such novel techniques: a lightweight ownership transfer system; a specialized resource alias analysis; and a system to create a fresh obligation when a non-final resource field is updated. Our approach occupies a unique slice of the design space: it is sound and runs relatively quickly (taking minutes on programs that a state-of-the-art approach took hours to analyze). We implemented our techniques for Java in an open-source tool called the Resource Leak Checker. The Resource Leak Checker revealed 49 real resource leaks in widely-deployed software. It scales well, has a manageable false positive rate (comparable to the high-confidence resource leak analysis built into the Eclipse IDE), and imposes only a small annotation burden (1/1500 LoC) for developers.