Resource-bound analysis aims to infer symbolic bounds of worst-case resource usage (e.g., running time and memory) of programs. Applications of resource analysis include job scheduling and prevention of side-channel attacks. Different resource-analysis techniques have complementary strengths and weaknesses. (Automatic) static resource analysis, which analyzes the source code of programs, is sound: if it successfully infers a cost bound, it is guaranteed to be a valid bound. However, due to the undecidability of resource analysis in general, every static analysis technique is incomplete: there exists a program that the analysis technique cannot handle. Meanwhile, data-driven analysis, which statistically analyzes cost measurements obtained by running programs on many inputs, can infer a candidate cost bound for any program. However, it does not guarantee soundness of inference results.

To overcome limitations of individual analysis techniques, this thesis develops hybrid resource analysis, which integrates two complementary analysis techniques via a user-adjustable interface. The user first specifies which analysis techniques should analyze which code fragments and quantities. Hybrid analysis then performs its constituent analysis techniques on their respective code fragments and quantities. Finally, their inference results are combined into an overall cost bound. Hybrid resource analysis retains the strengths of constituent analyses while gating their respective weaknesses.

The thesis introduces two hybrid-resource-analysis techniques: Hybrid AARA and resource decomposition. They adopt distinct designs of an interface between constituent analyses, posing a trade-off in the flexibility of hybrid analysis. Hybrid AARA integrates tatic resource analysis–Automatic Amortized Resource Analysis (AARA)–with data-driven resource analysis via a type-based interface. On the other hand, resource decomposition integrates different pairs of static, data-driven, and interactive resource analyses via a numeric-variable-based interface.

In addition to hybrid resource analysis, I discuss theoretical results of resource analysis: (i) the undecidability of resource analysis; and (ii) the polynomial-time completeness of Conventional AARA. I also describe newly developed Bayesian data-driven resource analysis, which statistically infers cost bounds by Bayesian inference. Finally, I present the optimization of probabilistic program-input generators by a genetic algorithm, showing that its output generator is more effective in triggering high computational cost than randomly generated inputs.

355 pages

Thesis Committee:
Jan Hoffmann (Chair)
Feras Saad
Matt Fredrikson
François Pottier (Inria Paris)

Srinivasan Seshan, Head, Computer Science Department
Martial Hebert, Dean, School of Computer Science

Creative Commons: CC-BY (Attribution)

Return to: SCS Technical Report Collection
School of Computer Science

This page maintained by reports@cs.cmu.edu