Integrating Resource Analyses via Resource Decomposition
Resource analysis aims to derive symbolic resource bounds of programs. Although numerous resource-analysis techniques have been developed— ranging from static to dynamic and manual to automated methods—they each come with their own distinct strengths and weaknesses. To overcome the limitations of individual resource-analysis techniques, a promising approach is to combine them in such a way that retains their complementary strengths while mitigating their respective weaknesses. To this end, this article proposes a novel resource-analysis framework called \emph{resource decomposition} that coherently integrates two analysis techniques in a way that enables powerful integrations that are infeasible using traditional “monolithic” approaches. The key idea of resource decomposition is to automatically transform an original program by identifying resource components that track custom quantities (e.g., recursion depths of specific functions) and serve as an interface between constituent analysis techniques. On the transformed program, one analysis technique is used to infer an overall cost bound parametric in the resource components, while other analysis techniques are used to infer symbolic bounds to be substituted for the resource components. The soundness of resource decomposition is established with a denotational cost semantics and a binary logical relation. It states that composing sound bounds results in a sound bound for the original program. Furthermore, we present three instantiations of the resource-decomposition framework, each representing distinct combinations of static, data-driven, and manual resource analyses. The data-driven part of these instantiations is a novel Bayesian approach to inferring linear and logarithmic bounds of recursion depths. An implementation and empirical evaluation of resource decomposition demonstrates that it can effectively infer sound and asymptotically tight cost bounds for a number of challenging benchmarks that are beyond the reach of previous analysis methods.