Lightweight and modular resource leak verification

“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.


A resource leak occurs when a program allocates a resource, such as a socket or file handle, but fails to deallocate it. Resource leaks are an important, common problem that cause resource starvation, slowdowns, and crashes. Previous techniques to prevent resource leaks are unsound, imprecise, inapplicable to existing code, slow, or a combination of these.

We observe that detecting a resource leak for a variable involves three parts: 1) tracking its must-call obligations, 2) tracking which methods have been called on it, and 3) comparing the results of these to check if its obligations have been fulfilled. Our key insight is that these 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. We developed a baseline leak checker via this approach. The precision of an accumulation analysis can be improved by computing targeted aliasing information, and we devised three novel techniques that use this capability to achieve precision in practice: 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 when compared to prior approaches: it is sound and runs quickly compared to heavier-weight approaches (running in 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 Plumber. Plumber revealed 45 real bugs in widely-deployed software. It scales well, has a manageable false positive rate (lower than the high-confidence resource leak analysis built into the Eclipse IDE), and imposes only a small annotation burden (1/2000 LoC) for developers.

BibTeX entry:

   author = {Martin Kellogg and Narges Shadab and Manu Sridharan and
	Michael D. Ernst},
   title = {Lightweight and modular resource leak verification},
   booktitle = {ESEC/FSE 2021: The ACM 29th joint European Software
	Engineering Conference and Symposium on the Foundations of
	Software Engineering (ESEC/FSE)},
   address = {Athens, Greece},
   month = aug,
   year = {2021}

(This webpage was created with bibtex2web.)

Back to Michael Ernst's publications.