FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
A General Equational Framework for Static Profiling of Parametric Resource Usage

Authors: Pedro Lopez-Garcia, Maximiliano Klemen, Umer Liqat and Manuel V. Hermenegildo

Paper Information

Title:A General Equational Framework for Static Profiling of Parametric Resource Usage
Authors:Pedro Lopez-Garcia, Maximiliano Klemen, Umer Liqat and Manuel V. Hermenegildo
Proceedings:LCC Contributed Talks
Editors: Erich Grädel and Jan Hoffmann
Keywords:Static Profiling, Static Analysis, Resource Usage Analysis, Complexity Analysis
Abstract:

ABSTRACT. For some applications, standard resource analyses do not provide the information required. Such analyses estimate the total resource usage of a program (without executing it) as functions on input data sizes. However, some applications require knowing how such total resource usage is distributed over selected parts of a program. We propose a novel, general, and flexible framework for setting up cost equations/relations which can be instantiated for performing a wide range of resource usage analyses, including both static profiling and the inference of the standard notion of cost. We extend and generalize standard resource analysis techniques, so that the relations generated include additional Boolean control variables for switching on or off different terms in the relations, as required by the desired resource usage profile. We also instantiate our framework to perform static profiling of accumulated cost (also parameterized by input data sizes). Such information is much more useful to the software developer than the standard notion of cost: it identifies the parts of the program that have the greatest impact on the total program cost, and which therefore should be optimized first. We also report on an implementation of our framework within the CiaoPP system, and its instantiation for accumulated cost, and provide some experimental results. In addition to generality, our new method brings important advantages over our previous approach based on a program transformation, including support for non-deterministic programs, better and easier integration in the compiler, and higher efficiency.

Pages:4
Talk:Jul 13 12:00 (Session 86F: LCC: Contributed Talks)
Paper: