Robust Resource Bounds with Static Analysis and Bayesian Inference
There are two approaches to automatically deriving symbolic worst-case resource bounds for programs: static analysis of the source code and data-driven analysis of cost measurements obtained by running the program. Static resource analysis is usually sound but incomplete. Data-driven analysis can always return a result, but its lack of robustness often leads to unsound results. This paper presents the design, implementation, and empirical evaluation of hybrid resource bound analyses that tightly integrate static analysis and data-driven analysis. The static analysis part builds on automatic amortized resource analysis (AARA), a state-of-the-art type-based resource analysis method that performs cost bound inference using linear optimization. The data-driven part is rooted in novel Bayesian modeling and inference techniques that improve upon previous data-driven analysis methods by reporting an entire probability distribution over likely resource cost bounds. A key innovation is a new type inference system called Hybrid AARA that coherently integrates Bayesian inference into conventional AARA, combining the strengths of both approaches. Hybrid AARA is proven to be statistically sound under standard assumptions on the runtime cost data. An experimental evaluation on a challenging set of benchmarks shows that Hybrid AARA (i) effectively mitigates the incompleteness of purely static resource analysis; and (ii) is more accurate and robust than purely data-driven resource analysis.
Fri 28 JunDisplayed time zone: Windhoek change
13:40 - 15:20 | |||
13:40 20mTalk | Scaling Type-Based Points-to Analysis with Saturation PLDI Research Papers Christian Wimmer Oracle Labs, Codrut Stancu Oracle Labs, David Kozak Brno University of Technology & Oracle Labs, Thomas Wuerthinger Oracle Labs DOI Pre-print | ||
14:00 20mTalk | Program Analysis for Adaptive Data Analysis PLDI Research Papers Jiawen Liu , Weihao Qu Monmouth University, Marco Gaboardi Boston University, Deepak Garg MPI-SWS, Jonathan Ullman Northeastern University DOI | ||
14:20 20mTalk | Robust Resource Bounds with Static Analysis and Bayesian Inference PLDI Research Papers Long Pham Carnegie Mellon University, Feras Saad Carnegie Mellon University, Jan Hoffmann Carnegie Mellon University DOI | ||
14:40 20mTalk | Context-Free Language Reachability via Skewed Tabulation PLDI Research Papers Yuxiang Lei UNSW Sydney, Camille Bossut Georgia Institute of Technology, Yulei Sui UNSW Sydney, Qirun Zhang Georgia Institute of Technology DOI | ||
15:00 20mTalk | Static Analysis for Checking the Disambiguation Robustness of Regular Expressions PLDI Research Papers Konstantinos Mamouras Rice University, Alexis Le Glaunec Rice University, Wu Angela Li Rice University, Agnishom Chattopadhyay Rice University DOI |