Inference of Resource Management Specifications
Authors: 
Narges Shadab, Pritam Gharat, Shrey Tiwari, 
Michael D. Ernst, Martin Kellogg, Shuvendu K. Lahiri, Akash Lal, 
Manu SridharanAuthors Info & Claims
Article No.: 282, Pages 1705 - 1728
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. 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.
References
[1]
Cristiano Calcagno, Dino Distefano, Jérémy Dubreil, Dominik Gabi, Pieter Hooimeijer, Martino Luca, Peter W. O’Hearn, Irene Papakonstantinou, Jim Purbrick, and Dulma Rodriguez. 2015. Moving fast with software verification. In NFM 2015: 7th NASA Formal Methods Symposium. Pasadena, CA, USA. 3–11. https://doi.org/10.4204/eptcs.188.2
[2]
John Peter Campora, Sheng Chen, Martin Erwig, and Eric Walkingshaw. 2018. Migrating gradual types. In POPL 2018: Proceedings of the 45th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. Los Angeles, CA, USA. https://doi.org/10.1145/3158103
[3]
2023. Resource Leak Checker for must-call obligations. https://checkerframework.org/manual/#resource-leak-checker Accessed 29 July 2023
[4]
2023. Checker Framework Whole-Program Inference. https://checkerframework.org/manual/#whole-program-inference Accessed 28 March 2023
[5]
David G. Clarke, John M. Potter, and James Noble. 1998. Ownership types for flexible alias protection. In OOPSLA ’98: Object-Oriented Programming Systems, Languages, and Applications. Vancouver, BC, Canada. 48–64.
[6]
2023. Analyzing data flow in C#. https://codeql.github.com/docs/codeql-language-guides/analyzing-data-flow-in-csharp/ Accessed 28 March 2023
[7]
Eclipse developers. 2023. Avoiding resource leaks. hhttps://help.eclipse.org/2023-03/index.jsp?topic=org.eclipse.jdt.doc.usertaskstask-avoiding_resource_leaks.htm Accessed 24 March 2023
[8]
accessed 2023. Entity Framework Core. https://github.com/dotnet/efcore#entity-framework-core
[9]
Cormac Flanagan and K. Rustan M. Leino. 2001. Houdini, an annotation assistant for ESC/Java. In FME ’01: International Symposium on Formal Methods Europe 2001: Formal Methods for Increasing Software Productivity. Berlin, Germany. 500–517.
[10]
Jeffrey S. Foster, Manuel Fähndrich, and Alexander Aiken. 1999. A theory of type qualifiers. In PLDI ’99: Proceedings of the ACM SIGPLAN ’99 Conference on Programming Language Design and Implementation. Atlanta, GA, USA. 192–203. https://doi.org/10.1145/301618.301665
[11]
Pritam Gharat, Narges Shadab, Shrey Tiwari, Shuvendu Lahiri, and Akash Lal. 2023. Resource Leak Checker (RLC#) for C# code using CodeQL. https://github.com/microsoft/global-resource-leaks-codeql
[12]
Brian Hackett, Manuvir Das, Daniel Wang, and Zhe Yang. 2006. Modular checking for buffer overflows in the large. In ICSE 2006, Proceedings of the 28th International Conference on Software Engineering. Shanghai, China. 232–241. https://doi.org/10.1145/1134285.1134319
[13]
Vincent J. Hellendoorn, Christian Bird, Earl T. Barr, and Miltiadis Allamanis. 2018. Deep learning type inference. In ESEC/FSE 2018: The ACM 26th joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE). Lake Buena Vista, FL, USA. 152–162. https://doi.org/10.1145/3236024.3236051
[14]
Atsushi Igarashi, Benjamin C. Pierce, and Philip Wadler. 2001. Featherweight Java: a minimal core calculus for Java and GJ. ACM Transactions on Programming Languages and Systems, 23, 3 (2001), May, 396–450. coden:ATPSDT issn:0164-0925
[15]
InferSharp developers. 2023. InferSharp. https://github.com/microsoft/infersharp/wiki/InferSharp:-A-Scalable-Code-Analytics-Tool-for-.NET Accessed 24 March 2023
[16]
J. B. Kam and J. D. Ullman. 1977. Monotone Data Flow Analysis Frameworks. Acta Informatica, 7 (1977), 305–317.
[17]
Martin Kellogg, Daniel Daskiewicz, Loi Ngo Duc Nguyen, Muyeed Ahmed, and Michael D. Ernst. 2023. Pluggable type inference for free. In ASE 2023: Proceedings of the 38th Annual International Conference on Automated Software Engineering. Luxembourg.
[18]
Martin Kellogg, Narges Shadab, Manu Sridharan, and Michael D. Ernst. 2021. Lightweight and modular resource leak verification. In ESEC/FSE 2021: The ACM 29th joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE). Athens, Greece. 181–192. https://doi.org/10.1145/3468264.3468576
[19]
Martin Kellogg, Narges Shadab, Manu Sridharan, and Michael D. Ernst. 2022. Accumulation analysis. In ECOOP 2022 — Object-Oriented Programming, 33rd European Conference. Berlin, Germany. 10:1–10:31. https://doi.org/10.4230/DARTS.8.2.22
[20]
Steve Klabnik and Carol Nichols. 2018. The Rust Programming Language. No Starch Press. https://doc.rust-lang.org/stable/book/
[21]
accessed 2023. Lucene.NET is a high performance search library for .NET. https://lucenenet.apache.org/
[22]
Microsoft. accessed 2023. CodeQL. https://codeql.github.com
[23]
Zeina Migeed and Jens Palsberg. 2020. What is decidable about gradual types? In POPL 2020: Proceedings of the 47th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. New Orleans, LA, USA. https://doi.org/10.1145/3373104
[24]
Matthew M. Papi, Mahmood Ali, Telmo Luis Correa Jr., Jeff H. Perkins, and Michael D. Ernst. 2008. Practical pluggable types for Java. In ISSTA 2008, Proceedings of the 2008 International Symposium on Software Testing and Analysis. Seattle, WA, USA. 201–212. https://doi.org/10.1145/1390630.1390656
[25]
Yun Peng, Cuiyun Gao, Zongjie Li, Bowei Gao, David Lo, Qirun Zhang, and Michael Lyu. 2022. Static inference meets deep learning: a hybrid type inference approach for Python. In ICSE 2022, Proceedings of the 43rd International Conference on Software Engineering. Pittsburgh, PA, USA. 2019–2030. https://doi.org/10.1145/3510003.3510038
[26]
Luna Phipps-Costin, Carolyn Jane Anderson, Michael Greenberg, and Arjun Guha. 2021. Solver-Based Gradual Type Migration. In OOPSLA 2021, Object-Oriented Programming Systems, Languages, and Applications. Chicago, IL, USA. Article 111, 27 pages. https://doi.org/10.1145/3485488
[27]
Benjamin C. Pierce. 2002. Types and Programming Languages. MIT Press, Cambridge, MA, USA. https://doi.org/10.7551/mitpress/1104.003.0005
[28]
PMD developers. 2023. CloseResource. https://pmd.sourceforge.io/pmd-6.55.0/pmd_rules_java_errorprone.html#closeresource Accessed 24 March 2023
[29]
Michael Pradel, Georgios Gousios, Jason Liu, and Satish Chandra. 2020. TypeWriter: neural type prediction with search-based validation. In ESEC/FSE 2020: The ACM 28th joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE). Sacramento, CA, USA. 209–220. https://doi.org/10.1145/3368089.3409715
[30]
Narges Shadab, Pritam Gharat, Shrey Tiwari, Michael D. Ernst, Martin Kellogg, Shuvendu Lahiri, Akash Lal, and Manu Sridharan. 2023. Inference of Resource Management Specifications (Artifact). https://doi.org/10.5281/zenodo.8333055
[31]
Robert E. Strom and Shaula Yemini. 1986. Typestate: A programming language concept for enhancing software reliability. IEEE Transactions on Software Engineering, SE-12, 1 (1986), January, 157–171.
[32]
Bjarne Stroustrup. 1994. The Design and Evolution of C++. Addison-Wesley, Reading, Massachusetts.
[33]
Emina Torlak and Satish Chandra. 2010. Effective interprocedural resource leak detection. In ICSE 2010, Proceedings of the 32nd International Conference on Software Engineering. Cape Town, South Africa. 535–544. https://doi.org/10.1145/1806799.1806876
[34]
Frédéric Vogels, Bart Jacobs, Frank Piessens, and Jan Smans. 2011. Annotation inference for separation logic based verifiers. In International Conference on Formal Methods for Open Object-Based Distributed Systems. 319–333.
[35]
Zhiqiang Zuo, John Thorpe, Yifei Wang, Qiuhong Pan, Shenming Lu, Kai Wang, Guoqing Harry Xu, Linzhang Wang, and Xuandong Li. 2019. Grapple: A graph system for static finite-state property checking of large-scale systems code. In EuroSys. Dresden, Germany. 1–17. https://doi.org/10.1145/3302424.3303972
Index Terms
- Inference of Resource Management Specifications
Recommendations
Lightweight and modular resource leak verification
ESEC/FSE 2021: Proceedings of the 29th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software EngineeringA 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, ...
ARC++: effective typestate and lifetime dependency analysis
ISSTA 2014: Proceedings of the 2014 International Symposium on Software Testing and AnalysisThe ever-increasing reliance of today's society on software requires scalable and precise techniques for checking the correctness, reliability, and robustness of software. Object-oriented languages have been used extensively to build large-scale ...
From Leaks to Fixes: Automated Repairs for Resource Leak Warnings
ESEC/FSE 2023: Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software EngineeringResource leaks are a common and elusive source of bugs that can result in crashes and security vulnerabilities. The most effective technique to identify such leaks during development is static analysis. However, empirical studies show that in addition to ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
October 2023
2250 pages
Copyright © 2023 Owner/Author.
This work is licensed under a Creative Commons Attribution 4.0 International License.
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 16 October 2023
Published in PACMPL Volume 7, Issue OOPSLA2
Check for updates
Badges
Author Tags
Qualifiers
- Research-article
Funding Sources
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 228Total Downloads
- Downloads (Last 12 months)228
- Downloads (Last 6 weeks)25
Reflects downloads up to 20 Sep 2024
Other Metrics
Citations
View Options
Get Access
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in