一句话：提出基于不动点的资源管理规约自动推断，在 Java/C# 上推断出 85.5% 手写注解且几乎不增加误报。
资源泄漏指程序在不再需要有限资源后未能释放，常导致崩溃与性能问题。已有工作通过检查资源管理规约来预防泄漏，但需手工编写注解，阻碍实用。本文提出自动推断资源管理规约的新技术，使 specify-and-check 验证更易应用。该领域推断的难点在于资源管理规约与常见类型推断目标差异大；且即使代码未完全遵循规约，也需推断开发者意图。作者设计了一组捕捉真实编码模式的推断规则，形成有效的基于不动点的推断算法，并在面向 Java 和 C# 的两个系统中实现。实验表明，该技术能推断出基准中程序员手写注解的 85.5%，自动推断与手写注解下验证器的误报率几乎相同。
A resource leak occurs when a program fails to free some finite resource after it is no longer needed. Such leaks are a significant cause of real-world crashes and performance problems. Recent work proposed an approach to prevent resource leaks based on checking resource management specifications. A resource management specification expresses how the program allocates resources, passes them around, and releases them; it also tracks the ownership relationship between objects and resources, and aliasing relationships between objects. While this specify-and-verify approach has several advantages compared to prior techniques, the need to manually write annotations presents a significant barrier to its practical adoption. This paper presents a novel technique to automatically infer a resource management specification for a program, broadening the applicability of specify-and-check verification for resource leaks. Inference in this domain is challenging because resource management specifications differ significantly in nature from the types that most inference techniques target. Further, for practical effectiveness, we desire a technique that can infer the resource management specification intended by the developer, even in cases when the code does not fully adhere to that specification. We address these challenges through a set of inference rules carefully designed to capture real-world coding patterns, yielding an effective fixed-point-based inference algorithm. We have implemented our inference algorithm in two different systems, targeting programs written in Java and C#. In an experimental evaluation, our technique inferred 85.5% of the annotations that programmers had written manually for the benchmarks. Further, the verifier issued nearly the same rate of false alarms with the manually-written and automatically-inferred annotations.
@article{paperbot1878,
title = {Inference of Resource Management Specifications},
author = {Narges Shadab and Pritam Gharat and Shrey Tiwari and Michael D. Ernst and Martin Kellogg and Shuvendu K. Lahiri and Akash Lal and Manu Sridharan},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {OOPSLA2},
year = {2023},
doi = {10.1145/3622858}
}