Automated complexity analysis for imperative programs

Abstract

Unsere Arbeit widmet sich dem Problem der automatisierten Komplexitätsanalyse, welches alternativ auch als Problem der automatisierten Abschätzung des Ressourcenverbrauchs formuliert wird. Eine Lösung dieses Problems wird angestrebt durch die Entwicklung einer Quellcodeanalyse (im Folgenden Bound-Analyse genannt) zur Abschätzung der Ausführungskosten eines gegebenen Programms. Der Begriff Kosten wird, wie üblich, durch ein Kostenmodell definiert, welches jeder Programminstruktion eine Ausführungskost zuweist. Je nach Anwendungsgebiet können Ausführungskosten beispielsweise in Form der benötigten Zeit, der benötigten Energie oder der Anzahl auszuführender Operationen definiert werden. Unsere Bound-Analyse behandelt das gegebene Programm als ein mathematisches Objekt und schätzt die Ausführungskosten bzw. den Ressourcenverbrauch des Programms mittels automatisierter Anwendung mathematischer und logischer Methoden ab, ohne das Programm auszuführen. Eine gewonnene Abschätzung wird in Form eines symbolischen Ausdrucks über den Programmparametern angegeben. Wir denken, dass Bound-Analysen in den verschiedensten Bereichen von großem Nutzen sein können. In unserer Arbeit diskutieren wir Anwendungsszenarien in den Bereichen Software Profiling, Program Understanding, Program Verification, Software Security und Automatic Parallelization. In den letzten Jahren wurden großen Fortschritte im Bereich der Bound-Analysen erzielt. Gegenwärtige Bound-Analysen können die Ausführungskosten beeindruckend komplizierter Code-Beispiele vollautomatisch deduzieren. Dennoch sehen wir zwei maßgebliche Nachteile aktueller Ansätze im Bereich der Bound-Analysen: (1) Die existierenden Analysen skalieren nicht ausreichend, um den Quellcode ganzer Programme, welcher oft Tausende oder Hunderttausende Code-Zeilen umfasst, zu analysieren. (2) Obwohl gegenwärtige Ansätze hinreichend genaue Abschätzungen des Ressourcenverbrauchs vieler und vor allem diffiziler Code-Beispiele berechnen können, werden dennoch die Kosten mancher, durchaus natürlicher Schleifeniterationsschemata nur sehr unzuverlässig und ungenau ermittelt. Mit unserer Arbeit wollen wir dazu beitragen, beide Probleme zu überwinden: (1) Die Bound-Analyse, welche wir in vorliegender Arbeit präsentieren, geht das Problem mangelnder Skalierbarkeit mittels einfacher statischer Analyse an: Während existierende Bound-Analysen mächtige Werkzeuge wie z.B. Abstract Interpretation, Computeralgebra oder lineare Optimierung verwenden, setzt unsere Analyse auf eine Reduktion des Problems mittels Programmabstraktion: In einem ersten Schritt abstrahieren wir das gegebene Programm in ein stark vereinfachtes Programmmodell. Anschließend wenden wir unseren Algorithmus für die Berechnung der Ausführungskosten auf dem vereinfachten Programm an. (2) Unsere Analyse erweitert die Möglichkeiten der Bound-Analyse: Wir erhalten asymptotisch präzise Abschätzungen der Kosten bzw. des Ressourcenverbrauchs für Instanzen einer Klasse von Schleifeniterationsschemata, für welche existierende Analysen meist fehlschlagen oder nur grobe Abschätzungen deduzieren können. Instanzen dieser Iterationsschemata werden häufig in Parser-Implementierungen sowie in String-Matching-Routinen verwendet. Wir diskutieren mehrere Beispiele in unserer Arbeit. Darüber hinaus ist unsere Analyse in der Lage, den überwiegenden Teil der in der Literatur diskutierten Bound-Analyse-Probleme zu lösen. Unsere Bound-Analyse basiert auf dem abstrakten Programmmodell der Difference Constraints. Difference Constraints wurden für die Terminationsanalyse eingeführt und bezeichnen relationale Ungleichungen der Form x' <= y + c. Eine solche Ungleichung drückt aus, dass der Wert von x im gegenwärtigen Zustand höchstens so groß ist wie der Wert von y im vorherigen Zustand, erhöht um eine ganzzahlige Konstante c. Wir denken, dass Difference Constraints, neben ihrer Anwendung in der Terminationsanalyse, auch eine gute Wahl für die Komplexitätsanalyse imperativer Programme darstellen, da die Komplexität solcher Programme meist aus dem Zusammenspiel von Zählerinkrementen bzw. -dekrementen der Form x := x + c und Zähler-Resets der Form x := y (wobei x != y) resultiert, diese Operationen können mittels der Difference Constraints x' <= x + c und x' <= y modelliert werden. Unsere Arbeit trägt zur Entwicklung von Bound-Analyse-Techniken wesentlich bei durch: (1) Effiziente Abstraktionstechniken: Wir zeigen, das Difference Constraints ein adäquates abstraktes Programmmodell für die Bound-Analyse bilden. (2) Einen neuen Bound-Analyse-Algorithmus: Wir definieren und diskutieren einen Algorithmus, welcher den Bereich der Bound-Analysen auf eine Klasse schwer zu analysierender, aber natürlich vorkommender Schleifeniterationsschemata ausweitet. Wir beweisen die Korrektheit unseres Algorithmus. (3) Eine skalierende Bound-Analyse: Unsere Analyse skaliert wesentlich besser als existierende Bound-Analysen. Unser Beitrag wird durch einen sorgfältigen experimentellen Vergleich auf Drei verschiedenen Benchmarks unterstützt: Wir vergleichen unsere Implementierung mit gegenwärtigen Bound-Analyse-Tools auf (a) einer großen Benchmark, bestehend aus C-Code, (b) einer Benchmark, welche Code-Beispiele aus der Literatur enthält, und (c) einer Benchmark, welche schwierige Schleifeniterationsschemata beinhaltet, die wir aus dem Quellcode echter Programme extrahiert haben. Wie die meisten existierenden Ansätze im Bereich der Bound-Analysen zielt unsere Analyse auf eine obere Abschätzung der Ausführungskosten.

Our work contributes to the field of automated complexity and resource bound analysis (bound analysis) that develops source code analyses for estimating the cost of running a given piece of software. The term cost is usually defined by a cost model which assigns an execution cost to each program instruction or operation. Depending on the application domain, the cost is estimated, e.g., in terms of consumed time, consumed power, or the number of executed statements. A bound analysis treats the program under scrutiny as a mathematical object, inferring a bound on the execution cost (with respect to the given cost model) by means of automated formal reasoning. The computed bound is usually expressed by a symbolic expression over the program's parameters. We argue that bound analysis could be applied with great benefits, e.g., in the areas of software profiling, program understanding, program verification, software security, and automatic parallelization. We state several application scenarios in this thesis. In recent years, the research on bound analysis has made great progress. State-of-the-art bound analysis techniques can automatically infer execution costs for impressively complicated code examples. Nevertheless, we see two main drawbacks of current bound analysis techniques: (1) Present approaches do not scale sufficiently for analyzing real code, which often consist of thousands or hundreds of thousands of lines of code with many nested conditionals. (2) Though existing approaches can infer tight bounds for many challenging examples, they nevertheless grossly over-approximate the cost of certain code patterns that are common in real source code. With our work we aim towards overcoming both problems: (1) The bound analysis we present in this work tackles the scalability problem by simple static analysis: In contrast to existing bound analysis techniques, which employ general purpose reasoners such as abstract interpreters, computer algebra tools or linear optimizers, we take an orthogonal approach based on the well-known program abstraction methodology: We first abstract a given program into an abstract program model by means of static analysis. We then apply our bound algorithm on the abstracted program, which is a simplified version of the original program. (2) Our bound algorithm extends the range of bound analysis. It infers tight bounds for a class of loop iteration patterns on which existing approaches fail or infer bounds that are not tight. Instances of such loop iterations can often be found in parsing and string matching routines. We state several examples in this work. At the same time our approach is general and can handle most of the bound analysis problems which are discussed in the literature. Our bound analysis is based on the abstract program model of difference constraints. Difference constraints have been used for termination analysis in the literature, where they denote relational inequalities of form x' <= y + c, and describe that the value of x in the current state is at most the value of y in the previous state plus some integer constant c. Intuitively, difference constraints are also a good choice for complexity and resource bound analysis because the complexity of imperative programs typically arises from counter increments resp. decrements of form x := x + c and resets of form x := y (where x != y), which can be modeled naturally by the difference constraints x' <= x + c resp. x' <= y + 0. Our work contributes to the field of automated complexity and resource bound analysis by: (1) Providing efficient abstraction techniques and demonstrating that difference constraints are a suitable abstract program model for automatic complexity and resource bound analysis. (2) Providing a new, soundness proven bound algorithm which extends the range of bound analysis to a class of challenging but natural loop iteration patterns that can be found in real source code. (3) Presenting a bound analysis technique which is more scalable than existing approaches. Our contributions are supported by a thorough experimental comparison on three benchmarks: We compare our implementation to other state-of-the-art bound analyses (a) on a large benchmark of real-world C code, (b) on a benchmark built of examples taken from the bound analysis literature and (c) on a benchmark of challenging iteration patterns which we found in real source code. As most approaches to bound analysis, our analysis infers upper bounds on the execution cost of a program.