| Title | Inference of resource management specifications |
| Publication Type | Conference Paper |
| Year of Publication | 2023 |
| Authors | Shadab N, Gharat P, Tiwari S, Ernst MD, Kellogg M, Lahiri S, Lal A, Sridharan M |
| Conference Name | OOPSLA 2023, Object-Oriented Programming Systems, Languages, and Applications |
| Date or Month Published | October |
| Conference Location | Cascais, Portugal |
| Abstract | 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. We recently proposed an approach to prevent resource leaks based on checking \textitresource 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. \par 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. \par We have implemented our inference algorithm in two different systems, targeting programs written in Java and C\#. In an experimental evaluation, 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. |
| Downloads | https://checkerframework.org/ implementation
|
| Citation Key | ShadabGTEKLLS2023 |
