Bounds for variables and loops: better together

Abstract

Ein Großteil heutzutage eingesetzter Software läuft in Umgebungen, die nur einen eingeschränkten Verbrauch von physischen Ressourcen (z.B. Speicher, Energie, Netzwerkverkehr, Zeit) erlauben. Mobile Geräte haben eine beschränkte Kapazität an Energie; und eingebettete Systeme werden mit minimalen Speicher ausgestattet. Die Frage nach dem Ressourcenverbrauch eines Programms kann oft auf das Problem reduziert werden, wie oft eine Schleife, die eine gegebene Ressource verbraucht, durchlaufen wird. Jüngste Methoden berechnen Schleifenschranken in modularer Art. Zuerst werden Schranken mit Programmvariablen ausgedrückt, die am Schleifenkopf definiert sind. Anschließend werden diese Schranken in Ausdrücke über die Programmparameter zurückübersetzt. Diese Aufgabe kann wiederum auf die Berechnung von Invarianten zurückgeführt werden, welche die möglichen Werte von Variablen nach oben hin beschränken. Aktuell eingesetzte Methoden der Invariantengenerierung sind unzureichend für die Analyse von Schranken; sie skalieren nicht für nicht-lineare und disjunktive Invarianten, die notwendig sind im Falle von verschachtelten Schleifen und Schleifen mit komplexem Kontrollfluss. Wir empfehlen Schranken für Schleifen und Variablen gemeinsam zu berechnen. Die zugrundeliegende Beobachtung ist, dass Schleifenschranken mittels Variablenschranken ausgedrückt werden können und umgekehrt - sie bilden eine wechselseitige Rekursion. Zum Beispiel kann der Wertzuwachs einer Variablen in einer Schleife, die in jeder Wiederholung die Variable um den Wert zwei inkrementiert, abgeschätzt werden, indem man die Schleifenschranke mit zwei multipliziert. Wir demonstrieren die Leistungsfähigkeit unseres Ansatzes durch eine umfassende experimentelle Evaluierung. Wir zeigen, dass unsere Methode für Programme effektiv ist, die in der Praxis eingesetzt werden oder in verwandter Literatur zu finden sind. Wir zeigen zudem, dass unsere Analyse andere Techniken an Leistungsfähigkeit übertrifft.

A great part of today's used software has one point in common: software programs are running in an environment inherently constrained by physical resources such as power, network-traffic, time and memory. A mobile device has a limited amount of energy; and an embedded system is equipped with minimal memory. How much of a resource a program may consume can often be reduced to the question how many times a loop is executed that contains a program location using this resource. Recent techniques aim to compute loop bounds in a modular way. At first, a bound is computed for each loop that is expressed in terms of program variables defined immediately before the loop. Next, each bound is translated into an expression over the procedure inputs. This task can be reduced to the problem of invariant generation. State-of-the-art invariant generation techniques are mostly insufficient for the purpose of bound analysis; they do not scale to non-linear or disjunctive invariants, which are required to shape bounds in presence of nested loops or loops with complex control flow. We propose a bound analysis that connects loop and variable bound computation. The underlying observation is that loop and variable bounds can be expressed in terms of each other - they build a mutual recursion. For example, if a program variable is incremented in every iteration of a loop by two, the overall increase of the variable's value due to that loop is bounded by the loop bound multiplied by two. We show that our method works effectively on patterns typically occurring in real-world programs and on examples posed in related literature. We demonstrate that our method outperforms existing techniques.