Download: implementation, scripts and data.
“Lightweight and modular resource leak checking (extended version)”
by Narges Shadab, Pritam Gharat, Shrey Tiwari,
Michael D. Ernst,
Martin Kellogg,
Shuvendu K. Lahiri,
Akash Lal, and
Manu Sridharan.
Software Tools for Technology Transfer, 2025.
A previous version appeared as
“Lightweight and modular resource leak verification”
by
Martin Kellogg,
Narges Shadab,
Manu Sridharan,
and
Michael D. Ernst.
In ESEC/FSE 2021: The ACM 29th joint European Software Engineering
Conference and Symposium on the Foundations of Software Engineering
(ESEC/FSE), (Athens, Greece), Aug. 2021, pp. 181-192.
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). Moreover, our approach generalizes to multiple analysis backends. RLC# revealed 49 real resource leaks in widely-deployed software; RLC# revealed 24 real resource leaks in five programs, including three Azure microservices. Both implementations scale well, have manageable false positive rates (comparable to heuristic bug-finders), and impose only a small annotation burden (about 1/6000 LoC) for developers.
This is an extended version of an ESEC/FSE 2021 publication. The key new contribution of this work is the introduction of the RLC# tool for checking of C# code. We describe the implementation of RLC# as a reachability-based analysis built on CodeQL (quite different than the previous approach) and present an evaluation of its effectiveness.
Download: implementation, scripts and data.
BibTeX entry:
@article{ShadabGTEKLLS2025,
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},
title = {Lightweight and modular resource leak checking (extended version)},
journal = {Software Tools for Technology Transfer},
year = {2025}
}
(This webpage was created with bibtex2web.)
Back to Michael Ernst's publications.