Implementing Hybrid Resource Analysis in Resource Aware ML
summary
Implements automated resource decomposition inside RaML 2 to combine sound static AARA bounds with data‑driven estimates of recursion depth, adding ghost recursion‑depth parameters via a type‑directed program transformation and lifting effectful expressions into a monad. Evaluates on mergesort, red‑black tree insert/delete/query and other functional programs, running the data‑driven analyzer on 200 randomly generated samples to infer logarithmic depth and substitute it into RaML 2’s multivariate bound to produce tight, sound O(n log n) costs.
AI-written summary · about
chapters (10)
- 0:00Hybrid resource analysis intro
- 1:04RAML limitations and hybrid need
- 2:08Resource decomposition process
- 3:11RAML 2 architecture
- 4:56Data-driven analysis integration
- 5:40Evaluation results
- 7:23Q&A: red-black trees
- 8:25New RAML 2 challenges
- 9:49Q&A: precision issues
- 11:16Summary and future
related talks
39mA Reusable Machine-Calculus for Automated Resource Analyses
15mRaising Expectations: Automating Expected Cost Analysis with Types
15mFaster Reachability Analysis for LR(1) Parsers
37mContractions Are Abstractions - Towards Effective Memory Management in ReML
15mA Modular Cost Analysis for Probabilistic Programs
18mReductive Analysis with Compiler-Guided Large Language Models for Input-Centric Code(…)
14mSound and Modular Activity Analysis for Automatic Differentiation in MLIR
34mModular Storage Mode Analysis