Automatic Resource Bound Analysis and Linear Optimization

on YouTube ↗48m

" summary

Automatic system generates symbolic worst‑case resource bounds by encoding type‑based potential annotations into linear constraints and solving them with LP solving (CLP/clex). Implementation targets a subset of OCaml (≈12k LOC) and exposes a web interface; benchmarks include standard list libraries and a verified C compiler extracted to OCaml. Solver instances grow to about 1M constraints and solve in ≈1 minute; derived multivariate polynomial bounds (binomial basis) are often asymptotically tight and match measured step counts on worst‑case inputs.

AI-written summary · about

" chapters (24)

1. 0:00Intro
2. 0:53Resource Usage in Safety-Critical Systems
3. 1:38Performance Bugs are common and Expensive
4. 2:45Software Security
5. 4:13Static Resource Bound Analysis
6. 5:12Research Challenges
7. 6:22Why is this Related?
8. 10:01Idea: Automate Amortized Analysis
9. 11:29Example: Append for Persistent Lists
10. 12:24Example: Composing Calls of Append
11. 17:48Example: Polynomial Potential Functions
12. 20:15Multivariate Resource Polynomials [POPL'11]
13. 21:21Resource Polynomials: Examples
14. 24:12Automatic Computation of the Bounds
15. 25:00Outline
16. 25:24Resource Aware ML
17. 28:38Macro Benchmarks
18. 31:04Machine Learning Cost Models
19. 31:58Bound for List Append on x86
20. 33:36Network-Flow Problems
21. 34:49Linear Constraints have a Simple Form
22. 38:00Most Complex Constraints: Sharing
23. 39:50Constraint Solving in Practice
24. 41:23Automatic Amortized Resource Analysis