PhD Defense
The IMDEA Software Institute researcher Maximiliano Klemen has successfully defended his PhD thesis on: “A General Framework for Static Resource Analysis and Profiling of (Parallel) Programs and an Application to Runtime Checking”, supervised by Prof. Pedro López, on March 5th.
The goal of static cost analysis is to automatically estimate the resources used by program executions without running the programs with concrete data, as functions of input data sizes and possibly other (environmental) parameters. In this thesis he improves and extends state-of-the-art static cost analysis techniques by developing a novel, general and flexible framework for resource usage analysis that can be easily instantiated to infer a wide range of resources, notions of costs, and approximations, which can deal with different programming languages, platforms and execution models.
For some applications, standard resource analyses, which estimate the total resource usage of a program, do not provide the information required. For example, helping developers make resource-related design decisions requires knowing how such total resource usage is distributed over selected parts of a program. The novel, general, and flexible framework developed in Maximiliano’s thesis solves this problem, by allowing setting up cost relations that can be instantiated for performing a wide range of resource usage analyses, including both static profiling and the standard notion of cost. He shows how to instantiate such framework to perform static profiling of accumulated cost (also parameterized by input data sizes). Such information identifies the parts of the program that have the greatest impact on the total program cost.
Moreover, parallel computing has become the dominant paradigm in computer architecture, and predicting resource usage on such platforms poses a difficult challenge. We address it by extending and instantiating our general framework for performing resource usage analysis of parallel (logic) programs. Besides cost functions, the analysis also infers other useful information to better exploit and assess the potential and actual parallelism of a system. He also develops a novel application of his cost analysis framework: inferring static performance guarantees for programs with run-time checks. Instrumenting programs for performing run-time checking of properties, such as regular shapes, is a common and useful technique that helps programmers detect incorrect program behaviors. However, such run-time checks inevitably introduce run-time overhead (in execution time, memory, energy, etc.). He proposes a method that uses static analysis to estimate such overhead. This approach can provide guarantees for all possible execution traces, and allows assessing how the overhead grows as the size of the input, which is a parameter of the estimated cost functions, grows. His method also extends an existing assertion verification framework to express “admissible” overheads, and statically and automatically checks whetherthe instrumented program conforms with such specifications.
The accuracy and applicability of his framework strongly depend on the capabilities of the component in charge of solving (or safely approximating) the cost and size recurrence relations generated during the analysis. In this thesis he proposes techniques for solving recurrence relations that extend state-of-the-art solvers, addressing some of their limitations. In particular, he develops a novel approach for solving arbitrary, constrained recurrence relations. It is a guess and check approach that uses well-known machine learning techniques for the guess stage, and a combination of an SMT-solver and a Computer Algebra System for the check stage. Additionally, he develops a method for solving cost relations involving a maximization operator, which appears when representing complex size and cost relations.
Finally, he reports on the implementation of the techniques developed in this thesis within the CiaoPP system and their experimental evaluation, obtaining encouraging results.
