Liquid resource types
Abstract
This article presents liquid resource types, a technique for automatically verifying the resource consumption of functional programs. Existing resource analysis techniques trade automation for flexibility – automated techniques are restricted to relatively constrained families of resource bounds, while more expressive proof techniques admitting value-dependent bounds rely on handwritten proofs. Liquid resource types combine the best of these approaches, using logical refinements to automatically prove precise bounds on a program’s resource consumption. The type system augments refinement types with potential annotations to conduct an amortized resource analysis. Importantly, users can annotate data structure declarations to indicate how potential is allocated within the type, allowing the system to express bounds with polynomials and exponentials, as well as more precise expressions depending on program values. We prove the soundness of the type system, provide a library of flexible and reusable data structures for conducting resource analysis, and use our prototype implementation to automatically verify resource bounds that previously required a manual proof.
Document Details
- Document Type
- Pub Defense Publication
- Publication Date
- Aug 02, 2020
- Source ID
- 10.1145/3408988
Entities
People
- A. Reynolds
- Di Wang
- Jan Hoffmann
- Nadia Polikarpova
- Tristan Knoth
Organizations
- Carnegie Mellon University
- Defense Advanced Research Projects Agency
- National Science Foundation
- University of California, San Diego