Selectively-Amortized Resource Bounding

Lu, Tianhan

Graduate Thesis Or Dissertation

Selectively-Amortized Resource Bounding Public Deposited

Analytics

Download PDF

Citations

Citeable URL: https://scholar.colorado.edu/concern/graduate_thesis_or_dissertations/tm70mw806

Abstract

Managing resource usage has become a critical concern for software developers as software development continues to grow in complexity. This thesis focuses on the practical aspects of automatically proving resource bounds by investigating how to bound an integer-valued resource variable by a given program expression. The automatic resource bound analysis has become increasingly important in detecting performance bugs, preventing algorithmic-complexity attacks, and identifying side-channel vulnerabilities. This thesis puts forth a novel paradigm of selectively-amortized resource bounding for practical yet sound analysis of resource usage.

The most simple and common approach, which we refer to as the worst-case reasoning, involves reducing the problem to the reachability bound problem. This method infers the maximum number of times a location can be visited, multiplies it by the worst-case cost at this location among all visits, and sums up such products for all locations. However, this approach fails to work for non-terminating programs like reactive programs, as the number of times a location can be reached may be unbounded.

To address this limitation, we adapt worst-case reasoning to work with non-terminating programs by introducing counters—auxiliary variables that track the number of times a location is reached—and specifying inductive relations that describe the worst-case reasoning using these counters. To handle unboundedness, we infer additional invariants about counters that describe the control flow. This approach is type-directed, and the inductive relations can be viewed as refinement types that can be validated by a type checking system.

However, worst-case reasoning, including the aforementioned type-directed approach, can become highly imprecise when the costs at a location vary widely among various iterations. This situation is particularly common in the design and analysis of leading data structures and algorithms that take advantage of amortization to achieve better overall performance, such as dynamic arrays and search structures. To address the imprecision that arises due to wide cost variations, one remedy is to use the most precise reasoning, which we dub fully-amortized reasoning. This approach accurately approximates the total resource usage before and after a transition by inferring flow-sensitive invariants. However, the practicality of this approach is limited since the required invariants are often complex polynomials that can be challenging to reliably infer.

This thesis introduces and focuses around a novel paradigm called selectively-amortized reasoning, which combines the simplicity of worst-case reasoning with the precision of fullyamortized reasoning. Selectively-amortized reasoning defines a spectrum of analysis by adjusting the analysis precision and simplicity, with worst-case reasoning being the simplest and fullyamortized reasoning being the most precise. To analyze a trace’s total resource usage, one decomposes the trace into subtraces, applies fully-amortized reasoning within each subtrace, and applies worst-case reasoning among the subtraces. We provide a formal proof that arbitrary selectivelyamortized reasoning soundly approximates the actual resource usage.

However, selecting the appropriate decomposition is critical, and to address this issue, this thesis proposes two automated approaches for searching for decompositions that simplify the required invariants while maintaining the best precision. The first approach is based on static analysis, specifically data dependency, while the second approach is based on dynamic analysis, including fuzzing and decision tree learning. To demonstrate the effectiveness of selectively-amortized reasoning in verifying resource bounds, we experimentally evaluate our search algorithms.

To summarize, this thesis presents a practical approach for software developers to manage resource usage that combines simplicity and precision, while also offering a range of analysis. We posit that selectively-amortized resource bounding provides a practical means to address the challenges of resource bound analysis.

Creator