Doctoral Thesis Oral Defense - Long Pham

— 12:00pm

Location:
In Person and Virtual - ET - Reddy Conference Room, Gates Hillman 4405 and Zoom

Speaker:
LONG PHAM , Ph.D. CandidateComputer Science DepartmentCarnegie Mellon University
https://www.cs.cmu.edu/~longp/

Hybrid Resource-Bound Analyses of Programs

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 mitigating 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 static 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.

Thesis Committee
Jan Hoffmann (Chair)
Feras Saad
Matt Fredrikson
Francois Pottier (Inria, Paris)

In Person and Zoom Participation.  See announcement. 
 

For More Information:
matthewstewart@cmu.edu

Add event to Google
Add event to iCal