Selectively-Amortized Resource Bounding
summary
Presents a framework that proves resource bounds by mixing worst-case and amortized reasoning, proves any partitioning into amortization segments sound, and gives an algorithm that finds minimal non-interfering segments so amortization only requires a single input variable per segment. Implements the analyzer and evaluates it on 4 Java libraries plus randomized loop idioms, showing selectively-amortized reasoning proves more bounds than pure worst-case and is more robust than fully-amortized analysis, which can be brittle.
AI-written summary · about
chapters (5)
- 0:00Start
- 0:03Resource Bounding
- 0:19Why Do We Need To Balance Resources
- 5:07Amortized Reasoning
- 6:15Selectively Amortized Reasoning
related talks
14mQuantified Underapproximation via Labeled Bunches
01h 09mThere's Treasure Everywhere
01h 02mPractical Memory Pool Based Allocators For Modern C++
57m“An allocator model for std2”
21mExact Loop Bound Analysis
18mInference of Resource Management Specifications
22mExecution Time Program Verification With Tight Bounds
01h 03mConstructing Generic Algorithms: Principles and Practice