Lightweight and modular resource leak verification

Martin Kellogg, Narges Shadab, Manu Sridharan, Michael D. Ernst

Research output: Chapter in Book/Report/Conference proceedingConference contribution

8 Scopus citations

Abstract

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.

Original languageEnglish (US)
Title of host publicationESEC/FSE 2021 - Proceedings of the 29th ACM Joint Meeting European Software Engineering Conference and Symposium on the Foundations of Software Engineering
EditorsDiomidis Spinellis
PublisherAssociation for Computing Machinery, Inc
Pages181-192
Number of pages12
ISBN (Electronic)9781450385626
DOIs
StatePublished - Aug 20 2021
Externally publishedYes
Event29th ACM Joint Meeting European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/FSE 2021 - Virtual, Online, Greece
Duration: Aug 23 2021Aug 28 2021

Publication series

NameESEC/FSE 2021 - Proceedings of the 29th ACM Joint Meeting European Software Engineering Conference and Symposium on the Foundations of Software Engineering

Conference

Conference29th ACM Joint Meeting European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/FSE 2021
Country/TerritoryGreece
CityVirtual, Online
Period8/23/218/28/21

All Science Journal Classification (ASJC) codes

  • Artificial Intelligence
  • Software

Keywords

  • Pluggable type systems
  • accumulation analysis
  • resource leaks
  • static analysis
  • typestate analysis

Fingerprint

Dive into the research topics of 'Lightweight and modular resource leak verification'. Together they form a unique fingerprint.

Cite this