Doctoral Speaking Skills Talk - Long Pham

— 1:00pm

Location:
In Person - Newell-Simon 3305

Speaker:
LONG PHAM, Ph.D. Student, Computer Science Department, Carnegie Mellon University
https://www.cs.cmu.edu/~longp/

Resource-bound analysis aims to infer symbolic bounds of worst-case resource usage (e.g., running time, memory, and energy) of programs as functions of program inputs. Resource analysis has numerous applications, including job scheduling in cloud computing and prevention of side-channel attacks. Two approaches to resource analysis are static analysis and data-driven analysis. Static analysis reasons about programs' behaviors by examining their source code. Data-driven analysis first runs programs on many inputs to collect cost measurements and then statistically analyzes this dataset.

Static and data-driven resource analyses have complementary strengths and weaknesses. Static analysis is sound: any cost bound successfully inferred is guaranteed to be a valid bound. However, static analysis is incomplete: every analysis technique has a program that it cannot handle. On the other hand, data-driven analysis can infer a candidate cost bound for any program. However, it does not guarantee soundness of inference results.

In this talk, I describe my recent work (PLDI 2024) on hybrid resource analysis, which integrates static and data-driven analyses. Given a program, the user first specifies which analysis techniques are applied to which code fragments. The two analyses are then performed on their respective code fragments. Finally, their inference results are combined into an overall cost bound of the program. Hybrid resource analysis retains the strengths of constituent analyses while mitigating their respective weaknesses.

I start by introducing background on type-based resource analysis Automatic Amortized Resource Analysis (AARA). It automates the potential method from amortized analysis. I next introduce our first contribution: Bayesian data-driven resource analysis. Finally, I present Hybrid AARA, which integrates AARA and Bayesian data-driven analysis via a novel interface between linear programming and sample algorithms. 

Joint work with Feras Saad and Jan Hoffmann.

Presented in Partial Fulfillment of the CSD Speaking Skills Requirement

Add event to Google
Add event to iCal