Albert Albiol, Elvira and Arenas Sánchez, Purificación and Genaim, Samir and Puebla Sánchez, Alvaro Germán
Comparing Cost Functions in Resource Analysis.
In: "First international conference on Foundational and practical aspects of resource analysis, FOPARA'09", 06/11/2009 - 06/11/2009, Eindhoven, Holanda. ISBN 978-3-642-15330-3.
Cost functions provide information about the amount of resources required to execute a program in terms of the sizes of input arguments. They can provide an upper-bound, a lower-bound, or the average-case cost. Motivated by the existence of a number of automatic cost analyzers which produce cost functions, we propose an approach for automatically proving that a cost function is smaller than another one. In all applications of resource analysis, such as resource-usage veriﬁcation, program synthesis and optimization, etc., it is essential to compare cost functions. This allows choosing an implementation with smaller cost or guaranteeing that the given resource-usage bounds are preserved. Unfortunately, automatically generated cost functions for realistic programs tend to be rather intricate, deﬁned by multiple cases, involving non-linear subexpressions (e.g., exponential, polynomial and logarithmic) and they can contain multiple variables, possibly related by means of constraints. Thus, comparing cost functions is far from trivial. Our approach ﬁrst syntactically transforms functions into simpler forms and then applies a number of su!cient conditions which guarantee that a set of expressions is smaller than another expression. Our preliminary implementation in the COSTA system indicates that the approach can be useful in practice