Tight Worst-Case Bounds for Polynomial Loop Programs

In the literature, a lot of different “cost analysis” problems (also called “resource bound analysis,” etc.) have been studied (e.g. [1, 11, 13, 18, 19, 24, 26, 27]); several of them may be grouped under the following general definition. The countable resource problem asks about the maximum usage of a “resource” that accumulates during execution, and which one can explicitly count, by instrumenting the program with an accumulator variable and instructions to increment it where necessary. For example, we can estimate the execution time of a program by counting certain “basic steps”. Another example is counting the number of visits to designated program locations. Realistic problems of this type include bounding the number of calls to specific functions, perhaps to system services; the number of I/O operations; number of accesses to memory, etc. The consumption of resources such as energy suits our problem formulation as long as such explicit bookkeeping is possible (we have to assume that the increments, if not constant, are given by a monotone polynomial expression).

In this paper we solve the bound analysis problem for a particular class of programs, defined in [7]. The bound analysis problem is to find symbolic bounds on the maximal possible value of an integer variable at the end of the program, in terms of some integer-valued variables that appear in the initial state of a computation. Thus, a solution to this problem might be used for any of the resource-bound analyses above. In this work we focus on values that grow polynomially (in the sense of being bounded by a polynomial), and our goal is to find polynomial bounds that are tight, in the sense of being precise up to a constant factor.

The programs we study are expressed by the so-called core language. It is imperative, including bounded loops, non-deterministic branches and restricted arithmetic expressions; the syntax is shown in Fig. 1. Semantics is explained and motivated below, but is largely intuitive; see also the illustrative example in Fig. 2. In 2008, it was proved [7] that for this language it is decidable whether a computed result is polynomially bounded or not. This makes the language an attractive target for work on the problem of computing tight bounds. However, for the past ten years there has been no improvement on [7]. We now present an algorithm to compute, for every program in the language, and every variable in the program which has a polynomial upper bound (in terms of input values), a tight polynomial bound on its largest attainable value (informally, “the worst-case value”) as a function of the input values. The bound is guaranteed to be tight up to a multiplicative constant factor but constants are left implicit (for example a bound quadratic in n will always be represented as \(n^2\)). The algorithm could be extended to compute upper and lower bounds with explicit constant factors, but choosing to ignore coefficients simplifies the algorithm considerably. In fact, we have striven for a simple, comprehensible algorithm, and we believe that the algorithm we present is sufficiently simple that, beyond being comprehensible, offers insight into the structure of computations in this model.

In this section, we give some basic definitions, complete the presentation of our programming language and precisely state the main result.

The loop is “disjunctive” because its meaning is that in every iteration, any of the given transitions may be applied. The semantics is formalized by traces (Definition 4). A SDL does not specify the number of iterations; our analysis generates polynomials which depend on the number of iterations as well as the initial state. For this purpose, we now introduce \(\tau \)-polynomials where \(\tau \) represents the number of iterations.

\(\tau \) has a special status and does not have a separate component in the polynomial giving its value. If p is a \(\tau \)-polynomial, then \(p(v_1,\dots ,v_n)\) is the result of substituting each \(v_i\) for the respective \(x_i\); and we also write \(p(v_1,\dots ,v_n,t)\) for the result of substituting t for \(\tau \) as well. The set of \(\tau \)-polynomials in n variables (n known from context) is denoted .

Multi-polynomials and polynomial transitions are formed from \(\tau \)-polynomials just as previously defined and are used to represent the effect of a variable number of iterations. For example, the \(\tau \)-polynomial transition \({\langle x'_1,x'_2\rangle } = {\langle x_1,\ x_2+\tau x_1\rangle }\) represents the effect of repeating (\(\tau \) times) the assignment . The effect of iterating the composite command: has an effect described by \({\mathbf x}' = {\langle x_1,\ x_2+\tau x_1, \ x_3 + \tau x_2 + \tau ^2 x_1\rangle }\) (here we already have an upper bound which is not reached precisely, but is correct up to a constant factor). We denote the set of \(\tau \)-polynomial transitions by . We should note that composition \({\mathbf q}\circ {\mathbf p}\) over is performed by substituting \({\mathbf p}[i]\) for each occurrence of \(x_i\) in \(\mathbf q\). Occurrences of \(\tau \) are unaffected (since \(\tau \) is not part of the state). We make a couple of preliminary definitions before reaching our goal which is the definition of the simple disjunctive loop problem (Definition 6).

Note that in the lower-bound clause (2), the linear monomials of p are not multiplied, in the left-hand side, by the coefficient \(d_{\mathbf p}\); this sets, in a sense, a stricter requirement for them: if the trace maps x to \(x^2\) then the bound \(2x^2\) is acceptable, but if it maps x to x, the bound 2x is not accepted. The reader may understand this technicality by considering the effect of iteration: it is important to distinguish the transition \(x'_1 = x_1\), which can be iterated ad libitum, from the transition \(x'_1 = 2x_1\), which produces exponential growth on iteration. Distinguishing \(x'_1 = x_1^2\) from \(x'_1 = 2x_1^2\) is not as important. The result set \({\mathcal B}\) above is sometimes called a loop summary. We remark that Definition 6 implies that the max of all these polynomials provides a “big Theta” bound for the worst-case (namely biggest) results of the loop’s computation. We prefer, however, to work with sets of polynomials. Another technical remark is that \(c_{\mathbf p}, d_{\mathbf p}\) range over real numbers. However, our data and the coefficients of polynomials remain integers, it is only such comparisons that are performed with real numbers (specifically, to allow \(c_{\mathbf p}\) to be smaller than one).

We show how to reduce the problem of analysing core-language programs to the analysis of polynomially-bounded simple disjunctive loops.

Intuitively, evaluating abstractly consists of simulating any finite number of iterations, i.e., computingwhere . The question now is whether the sequence (1) reaches a fixed point. In fact, it often doesn’t. However, it is quite easy to see that in the multiplicative fragment of the language, that is, where the addition operator is not used, such non-convergence is associated with exponential growth. Indeed, since there is no addition, all our polynomials are monomials with a leading coefficient of 1 (monic monomials)—this is easy to verify. It follows that if the sequence (1) does not converge, higher and higher exponents must appear, which indicates that some variable cannot be bounded polynomially. Taking the contrapositive, we conclude that if all variables are known to be polynomially bounded the sequence will converge. Thus we have the following easy (and not so satisfying) result:

Observation 2 For a SDL that does not use addition, the sequence \(Q_i\) as in (1) reaches a fixed point, and the fixed point provides tight bounds for all the polynomially-bounded variables.

When we have addition, we find that knowing that all variables are polynomially bounded does not imply convergence of the sequence (1). An example is: yielding the infinite sequence of MPs \({\langle x_1,x_2,x_3\rangle }\), \({\langle x_1+x_2,x_2,x_3\rangle }\), \({\langle x_1+2x_2,x_2,x_3\rangle }\), ... Our solution employs two means. One is the introduction of \(\tau \)-polynomials, already presented. The other is a kind of abstraction—intuitively, ignoring the concrete values of (non-zero) coefficients. Let us first define this abstraction:

The meaning of abstract polynomials is given by the following rules:Analysing a SDL. To analyse a SDL specified by a set of MPs \({\mathcal S}\), we start by computing \(\alpha ({\mathcal S})\). The rest of the algorithm computes within . We define two operations that are combined in the analysis of loops. The first, which we call closure, is simply the fixed point of accumulated iterations as in the multiplicative case. It is introduced by the following two definitions.

Note that \({\mathbf t}^{\mathop {\bullet }(n)} = \alpha (\gamma ({\mathbf t})^{(n)})\), where \({\mathbf p}^{(n)}\) is defined using ordinary composition.

In the correctness proof, we argue that when all variables are polynomially bounded in a loop \({\mathcal S}\), the closure of \(\alpha ({\mathcal S})\) can be computed in finite time; equivalently, it equals \(\bigcup _{i=0}^{k} (\alpha ({{\mathcal S}}))^{\mathop {\bullet }(i)}\) for some k. The argument is essentially the same as in the multiplicative case.

Note that this is composition in the abstract domain. So, for instance, \({\langle x_1, x_2\rangle }\) is idempotent, and so is \({\langle x_1 + x_2, x_2\rangle }\), while \({\langle x_1x_2, x_2\rangle }\) and \({\langle x_1 + x_2, x_1\rangle }\) are not.

Note that the arithmetic here is abstract (see examples below). Note also that in the term \(\tau {\mathbf p}[i]'\) the \(\tau \) is already present in \(\mathbf p\), while in \(\tau {\mathbf p}[i]''\) it is added to existing monomials. In this definition, the monomials of \({\mathbf p}[i]'''\) are treated like those of \(\tau {\mathbf p}[i]'\); however, in certain steps of the proofs we treat them differently, which is why the notation separates them.

Finally we can present the analysis of the loop command.

We claim that our algorithm obtains a description of the worst-case results of the program that is precise up to constant factors. That is, we claim that the set of MPs returned provides an upper bound (on all executions) which is also tight; tightness means that every MP returned is also a lower bound (up to a constant factor) on an infinite sequence of possible executions. Unfortunately, due to space constraints, we are not able to give full details of the proofs here; however, we give the main highlights. Intuitively, what we want to prove is that the multi-polynomials we compute cover all “behaviors” of the loop. More precisely, in the upper-bound part of the proof we want to cover all behaviors: upper-bounding is a universal statement. To prove that bounds are tight, we show that each such bound constitutes a lower bound on a certain “worst-case behavior”: tightness is an existential statement. The main aspects of these proofs are as follows:

Bound analysis, in the sense of finding symbolic bounds for data values, iteration bounds and related quantities, is a classic field of program analysis [18, 24, 27]. It is also an area of active research, with tools being currently (or recently) developed including COSTA [1], AProVE [13], CiaoPP [19], \(C^4B\) [11], Loopus [26]—all for imperative programs. There is also work on functional and logic programs, term rewriting systems, recurrence relations, etc. which we cannot attempt to survey here. In the rest of this section we survey work which is more directly related to ours, and has even inspired it.

The LOOP language is due to Meyer and Ritchie [20], who note that it computes only primitive recursive functions, but complexity can rise very fast, even for programs with nesting-depth 2. Subsequent work [15‐17, 22] concerning similar languages attempted to analyze such programs more precisely; most of them proposed syntactic criteria, or analysis algorithms, that are sufficient for ensuring that the program lies in a desired class (often, polynomial-time programs), but are not both necessary and sufficient: thus, they do not prove decidability (the exception is [17] which has a decidability result for a weak “core” language). The core language we use in this paper is from Ben-Amram et al. [7], who observed that by introducing weak bounded loops instead of concrete loop commands and non-deterministic branching instead of “if”, we have weakened the semantics just enough to obtain decidability of polynomial growth-rate. Justifying the necessity of these relaxations, [8] showed undecidability for a language that can only do addition and definite loops (that cannot exit early).

In the vast literature on bound analysis in various forms, there are a few other works that give a complete solution for a weak language. Size-change programs are considered by [12, 28]. Size-change programs abstract away nearly everything in the program, leaving a control-flow graph annotated with assertions about variables which decrease (or do not increase) in a transition. Thus, it does not assume structured and explicit loops, and it cannot express information about values which increase. Both works yield tight bounds on the number of transitions until termination.

Dealing with a somewhat different problem, [14, 21] both check, or find, invariants in the form of polynomial equations. We find it remarkable that they give complete solutions for weak languages, where the weakness lies in the non-deterministic control-flow, as in our language. If one could give a complete solution for polynomial inequalities, this would have implied a solution to our problem as well.

We have solved an open problem in the area of analyzing programs in a simple language with bounded loops. For our language, it has been previously shown that it is possible to decide whether a variable’s value, number of steps in the program, etc. are polynomially bounded or not. Now, we have an algorithm that computes tight polynomial bounds on the final values of variables in terms of initial values. The bounds are tight up to constant factors (suitable constants are also computable). This result improves our understanding of what is computable by, and about, programs of this form. An interesting corollary of our algorithm is that as long as variables are polynomially bounded, their worst-case bounds are described tightly by (multivariate) polynomials. This is, of course, not true for common Turing-complete languages. Another interesting corollary of the proofs is the definition of a simple class of patterns that suffice to realize the worst-case behaviors. This will appear in a planned extended version of this paper.

There are a number of possible directions for further work. We would like to look for decidability results for richer (yet, obviously, sub-recursive) languages. Some possible language extensions include deterministic loops, variable resets (cf. [4]), explicit constants, and procedures. The inclusion of explicit constants is a particularly challenging open problem.

Rather than extending the language, we could extend the range of bounds that we can compute. In light of the results in [17], it seems plausible that the approach can be extended to classify the Grzegorczyk-degree of the growth rate of variables when they are super-polynomial. There may also be room for progress regarding precise bounds of the form \(2^{poly}\).

In terms of time complexity, our algorithm is polynomial in the size of the program times \({n^{nd}}\), where d is the highest degree of any MP computed. Such exponential behavior is to be expected, since a program can be easily written to compute a multivariate polynomial that is exponentially long to write. But there is still room for finer investigation of this issue.