Resource Analysis in the COSTA System

Having information about the execution cost of programs, i.e., the amount of resources that the execution will require, is useful for many different purposes, including program optimization, verification and certification. Reasoning about execution cost is difficult and error-prone. Therefore, it is widely recognized that cost analysis, sometimes also referred to as resource analysis or automatic complexity analysis, is quite important. COSTA (http://costa.ls.fi.upm.es) is a state-of-the-art cost and termination analyzer which automates this task. The system is able to infer upper and lower bounds on the resource consumption of a large class of programs. Given a program P, the analysis results allow bounding the cost of executing P on any input data x without having to actually run P(x).

The first successful proposal for automatically computing the complexity of programs was the seminal work of Wegbreit [33]. Since then, a number of cost analysis frameworks have been proposed, mostly in the context of declarative programming languages (functional programming [23, 27, 32, 28, 17] and logic programming [18, 25]). Cost analysis of imperative programming languages has received significantly less attention. It is worth mentioning the pioneering work of [1]. To the best of our knowledge, COSTA has been the first system which automatically infers bounds on cost for a large class of Java-like programs, getting meaningful results. The system is implemented in Prolog (it runs both on Ciao [20] and SWI Prolog [34]) and uses the Parma Polyhedra Library [16] for manipulating linear constraints. More info on COSTA is available from its  website, where it can be used from a web interface.

1 From Programs to Cost Relations

The classical approach to static cost analysis consists of two phases. First, given a program and a cost model, the analysis produces cost relations, i.e., a system of recursive equations which capture the cost of the program in terms of the size of its input data. In a second phase described below, the cost relations are solved into an upper and/or a lower bound. This first phase is in turn twofold:

Intermediate representation. The program is first transformed into a recursive intermediate representation (IR) [6]. The transformation starts by constructing the Control Flow Graph (CFG) of the program. Each block of the CFG is transformed into one rule in the IR. Iteration is transformed into recursion and conditional constructs are represented as multiple (mutually exclusive) guarded rules. Intermediate programs resemble declarative programs due to their rule-based form. However, they are still imperative, since they use destructive assignment and store data in mutable data structures (stored in a global memory or heap).

Generation of cost relations. A cost model declares the cost of each basic instruction of the language. COSTA incorporates a range of cost models for counting the number of executed instructions, the memory consumed, the number of invocations to a given method, among others. Given a program (in intermediate form) and a selection of a cost model, we automatically generate cost relations (CRs) which define the cost of executing the program w.r.t. the selected cost model. CRs are basically an extended form of recurrence relations defined by equations of this form ⟨c(x) = e,φ⟩, where e is a cost expression and φ is a set of linear constraints which define the applicability conditions for the equations and the size relations among the variables in the equation. The inference of φ is done by means of an abstract compilation of the program and a subsequent size analysis (see [4] for more details).

2 From Cost Relations to Closed-Form Bounds

Though CRs are simpler than the programs they originate from, since all variables are of integer type, in several respects they are not as static as one would expect from the result of a static analysis.

One reason is that they are recursive and thus we may need to iterate for computing their value for concrete input values. Another reason is that even for deterministic programs, it is well known that the loss of precision introduced by the size abstraction may result in cost relations which are non-deterministic. For both reasons, it is clear that it is interesting to compute closed-form upper bounds (UB for short) and lower bounds (LB) for the cost relation, whenever this is possible, i.e., bounds which are not in recursive form. For inferring closed-form bounds, COSTA relies on program analysis techniques instead of on purely mathematical approaches as those incorporated in computer algebra systems. Indeed, if one ignores the cost expressions in the equations, CRs are constraint logic programs, and existing techniques developed in the context of CLP can be easily adapted to reason on the equations. The choice of treating CRs as (CLP) programs is probably the main reason for which COSTA has succeeded where previous cost analyzers have failed.

Upper Bounds. The first step for inferring closed-form bounds consists in applying partial evaluation [22] to make all recursive calls in the CRs direct. This makes the loops, and their caller-callee relation, simpler and explicit. Then, an UB for each loop is inferred in a compositional manner by using one of the following two approaches. The first approach [4] consists in inferring an UB f(x₀) on the number of iterations of the loop and an UB on the worst-case cost e(x₀) of its iterations, and then f(x₀) * e(x₀) is a sound UB. Here, f is inferred by synthesizing a ranking function [26] for the corresponding loop and e by inferring a loop invariant and then using parametric integer programming [19]. This approach is widely applicable and reasonably precise. However, when the cost accumulated varies significantly from one iteration to another, taking the worst case cost for all iterations is too imprecise. The second approach [12] allows obtaining more precise UBs by simulating the variation from one iteration to the next one using recurrence relations. While this approach computes very precise UBs, it is less applicable that the first one.

Lower Bounds. In the latter approach, i.e., [12], the inference of LBs is a dual problem to that of inferring UBs. The main difference is that one has to use (new) techniques for inferring LBs on the number of iterations and for obtaining the best-case cost of each iteration.

Amortized cost analysis. There are programs for which amortized cost analysis [31] is required in order to produce precise UBs for them. In such programs, costly operations cannot occur with high frequency and thus taking their worst-case cost, as in CRs, would lead to a very imprecise bound. To overcome these limitations, we have recently developed [15] techniques based on a novel definition of CRs that involve input an output arguments, and a corresponding solving procedure that is based on real quantifier elimination. However, this subsystem is still prototypical and not fully integrated in COSTA.

3 Advanced Topics in Resource Analysis

We briefly overview some advanced topics in resource analysis which we have investigated within the context of the COSTA system.

3.1 Non-Cumulative Resources

The approach described so far can be used to estimate the accumulated cost along the program’s execution. Unfortunately, it is not suitable to infer non-cumulative resources (e.g., the peak memory consumption or the task-level described below). This is because non-cumulative resources require reasoning on all possible states to obtain their maximum.

Memory Consumption. In the context of languages with garbage collection, such as Java, the amount of data stored in the heap increases and decreases along the execution and, therefore, the interest is in estimating the maximum memory consumption (a.k.a. peak memory consumption). COSTA develops a novel approach [11, 10, 9] which is parametric on the notion of object lifetime, i.e., on when objects become collectible. If objects lifetimes are inferred by a reachability analysis, then our analysis infers accurate upper bounds on the memory consumption for a reachability-based garbage collector. Interestingly, if objects lifetimes are inferred by a heap liveness analysis, then we approximate the program minimal memory requirement, i.e., the peak memory usage when using an optimal garbage collector which frees objects as soon as they become dead. The key idea is to integrate information on objects lifetimes into the process of generating the recurrence relations which capture the memory usage at the different program states.

Task-Level. In parallel programs, the number of tasks which can be active at the same time is a valuable piece of information, which is also a non-cumulative type of resource. Knowledge on the task-level is useful to maximize the performance when the computation must be carefully distributed among the processors of a multicore architecture. COSTA features a static analysis [13] which can find upper bounds to the level of parallelism of programs written in languages (the analysis works on a subset of the X10 language [24]) whose concurrency model is based on the async and finish primitives. As before, the key idea is to integrate information on the lifetime of tasks into the recurrence relations.

3.2 Heap-Sensitive Analysis

Shared mutable data structures, such as those stored in the heap, are the bane of formal reasoning and static analysis. In object-oriented programs most data reside in objects and arrays stored in the heap. Analyses which keep track of heap-allocated data are referred to as heap-sensitive. The approach developed in COSTA [14, 5, 3] is based on the observation that, by analyzing scopes, rather than the application as a whole, it is often possible to keep track of heap accesses in a similar way to local variables. Under some locality conditions, heap accesses can be replaced by equivalent non-heap allocated ghost variables. The resulting program can then be the input to any heap-insensitive static analyzer, in particular, to the one that we already have in COSTA.

3.3 Incremental Resource Analysis

A key challenge for static analysis techniques is achieving a satisfactory combination of precision and scalability. Making precise (and hence expensive) static analysis incremental is a step forward in this direction. The difficulty when devising an incremental analysis framework is to recompute the least possible information and do it in the most efficient way. In other approaches to incremental analysis, such as in the logic programming context [21], the analysis is focused in a single abstract domain. In contrast, COSTA includes a multi-domain incremental analysis engine [7] which can be used by all global pre-analyses required to infer the resource usage of a program (including class analysis, sharing, cyclicity, constancy and size analysis). The algorithm is multi-domain in the sense that it interleaves the computation for the different domains and takes into account dependencies among them, in such a way that it is possible to invalidate only partial pre-computed information. A fundamental idea to minimize the amount of information which needs to be recomputed is to be able to distinguish within a cost summary the cost subcomponent associated to each method, so that the final cost functions can be recomputed by replacing only the affected subcomponents.

3.4 Concurrency and Distribution

In order to develop a resource analysis for distributed and concurrent programs, we have considered a concurrency model based on the notion of concurrently running (groups of) objects, similar to the actor-based and active-objects approaches [29, 30]. These models take advantage of the concurrency implicit in the notion of object in order to provide programmers with high-level concurrency constructs that help in producing concurrent applications more modularly and in a less error-prone way. We have incorporated in COSTA a static cost analysis [2, 8] for concurrent OO programs, which is parametric w.r.t. the notion of resource that can be instantiated to measure both traditional and concurrency-related resources. The main novelty of the analysis is that it provides the resource consumption per cost center, where each cost center represents a distributed component. Having anticipated knowledge on the resource consumption of the different components which constitute a system is useful for distributing the load of work. Upper bounds can be used to predict that one component may receive a large amount of remote requests, while other siblings are idle most of the time. Also, our framework allows instantiating the different components with the particular features of the infrastructure on which they are deployed.

Acknowledgments. This work was funded in part by the Information & Communication Technologies program of the European Commission, Future and Emerging Technologies (FET), under the ICT-231620 HATS project, by the Spanish Ministry of Science and Innovation (MICINN) under the TIN-2008-05624 and PRI-AIBDE-2011-0900 projects, by UCM-BSCH-GR35/10-A-910502 grant and by the Madrid Regional Government under the S2009TIC-1465 PROMETIDOS-CM project.

References