# Cost Analysis of Programs Based on the Refinement of Cost Relations

### Flores Montoya, Antonio (2017)Cost Analysis of Programs Based on the Refinement of Cost Relations. Technische Universität DarmstadtPh.D. Thesis, Primary publication

 Preview
Text
Thesis_Antonio_Flores.pdf - Published Version
Copyright Information: CC BY-NC-ND 4.0 International - Creative Commons, Attribution NonCommercial, NoDerivs.

Item Type: Ph.D. Thesis
Type of entry: Primary publication
Title: Cost Analysis of Programs Based on the Refinement of Cost Relations
Language: English
Referees: Hähnle, Prof. Dr. Reiner ; Giesl, Prof. Dr. Jürgen
Date: 28 August 2017
Date of oral examination: 14 July 2017
Abstract:

Cost analysis aims at statically inferring the amount of resources, such as time or memory, needed to execute a program. This amount of resources is the cost of the program and it depends on its input parameters. Obtaining a function (in terms of the input parameters) that represents the cost of a program precisely is generally not possible. Thus, cost analyses attempt to infer functions that represent upper or lower bounds of the cost of programs instead.

Many existing cost analyses approach the problem in two stages. First, the target program is transformed into an integer abstract representation where the resource consumption is explicit and second, the abstract representation is analyzed and cost bounds are inferred from it. The advantage of this approach is that the second part is language independent and resource independent. That is, it can be reused across different programming languages and to analyze the program cost with respect to different resources. Cost relations are a possible abstract representation. They are similar to constraint logic programs annotated with costs and they can easily represent both imperative and functional programs.

Existing cost analyses based on cost relations have limited support for programs that have a complex control flow, or present amortized complexity, that is, when the sum of the cost of the parts yields a higher asymptotic cost than the cost of the whole. This thesis identifies these limitations, and presents a new analysis of cost relations that overcomes them.

The analysis can obtain upper and lower bounds of programs expressed as cost relations and it contains three parts:

1. The first part reduces any mutually recursive cost relations to cost relations that only have direct recursion and performs some simplifications.

2. The second part consists of a refinement of cost relations that partitions all possible executions of the program into a finite set of execution patterns named chains. The refinement also infers precise invariants for each of the chains, discards unfeasible execution patterns and proves termination.

3. In the third part of the analysis, cost bounds are inferred compositionally. For that purpose, a novel cost representation, named cost structures, is presented. Cost structures reduce the computation of complex bounds to the inference of simple constraints using linear programming. They can represent polynomial upper and lower bounds of programs with max and min operators.

The analysis is proven sound with respect to a new semantics of cost relations. This semantics distinguishes between terminating and non-terminating executions and models the behavior of non-terminating executions accurately.

In addition, the analysis has been implemented in the tool CoFloCo and it has been extensively evaluated against other state-of-the-art tools and with respect to a variety of benchmarks. These benchmarks include imperative programs, functional programs, and term rewrite systems. CoFloCo performs well in all categories which demonstrates both the power of the analysis and its versatility.

Alternative Abstract:
Alternative AbstractLanguage

Die Kostenanalyse von Programmen ermöglicht es, den für die Ausführung eines Programmes notwendigen Ressourcenbedarf, wie zum Beispiel Zeit oder Speicher statisch, zu bestimmen. Den Ressourcenbedarf eines Programms bezeichnet man auch als die Kosten des Programms. Die Programmkosten hängen im Allgemeinen von Eingabeparametern (den Eingabedaten) ab. Das Bestimmen einer Funktion, die in Abhängigkeit von den Eingabeparametern die exakten Kosten eines Programms angibt, ist in der Regel nicht möglich. Stattdessen versucht man bei der Kostenanalyse Funktionen zu ermitteln, die obere und untere Schranken für die Kosten eines Programmes darstellen.

Viele der existierenden Ansätze zur Kostenanalyse gehen das Problem in zwei Stufen an. Zuerst wird das zu analysierende Programm in eine abstrakte Integer-Repräsentation überführt, in welcher der Ressourcenbedarf/-verbrauch explizit dargestellt ist. In der zweiten Stufe wird diese abstrakte Repräsentation analysiert und obere bzw. untere Schranken bestimmt. Der Vorteil dieses Ansatzes ist, dass die zweite Stufe unabhängig von der Programmiersprache und der betrachteten Ressource (Zeit, Speicher usw.) ist. Dies ermöglicht den Einsatz der für die zweite Stufe entwickelten Techniken und Werkzeuge zur Analyse von Programmen in unterschiedlichsten Programmiersprachen bzgl. des Verbrauchs unterschiedlich Ressourcen. Kostenrelationen bieten sich als eine Wahl für die abstrakte Repräsentationen der Programme an. Sie ähneln Programmen aus der Constraint-logischen Programmierung, die mit Kostenannotationen versehen sind. Kostenrelationen erlauben es ferner, funktionale sowie imperative Programme auf einfache Art zu repräsentieren.

Existierende Kostenanalysen haben eine Reihe von Nachteilen betreffend der Analyse von Programmen mit komplexem Kontrollfluss sowie bei der Bestimmung amortisierter Komplexität zur Beschreibung von Szenarien, bei denen die Gesamtkosten eines Programmes kleiner sind als die Summe der asymptotischen Einzelkosten. In dieser Arbeit werden die Einschränkungen der existierenden Ansätze identifiziert und eine neuartige Analyse entwickelt, die diese überwindet. Die entwickelte Analyse bestimmt obere und untere Schranken für in Kostenrelationen überführte Programme. Sie besteht aus den folgenden drei Teilen:

1. Im ersten Teil der Analyse werden wechselseitig-rekursive Kostenrelationen in äquivalente Kostenrelationen überführt, die nur noch einfache Rekursionen enthalten. Ausserdem werden weitere Vereinfachungsschritte durchgeführt.

2. Im zweiten Teil werden die Kostenrelationen mit Hinblick auf den Kontrollfluss verfeinert. Die Verfeinerung partitioniert die Kostenrelationen in eine endliche Menge von Ausführungsmustern, sogenannten Ketten (Chains), die alle möglichen Ausführungen beschreibt. Die Verfeinerung gibt des weiteren präzise Invarianten für die einzelnen Ketten an, eliminiert nicht erreichbare Programmpfade und beweist die Terminierung des Programms.

3. Im dritten Teil der Analyse werden schließlich Schranken für die Kosten auf kompositionelle Art und Weise berechnet. Zu diesem Zweck wird eine neuartige Art der Kostenrepräsentation, genannt Kostenstrukturen, entwickelt und vorgestellt. Kostenstrukturen erlauben es, die Berechnung komplexer Schranken auf das Lösen einfacher Constraints mit Hilfe linearer Programmierung zu reduzieren. Kostenstrukturen können polynomielle obere und untere Schranken von Programmen repräsentieren und unterstützen dabei max- und min-Operatoren.

Die entwickelte Analyse wird als korrekt bzgl. einer neuen Semantik von Kostenrelationen bewiesen. Die im Rahmen dieser Arbeit entwickelte neue Semantik erlaubt es, zwischen terminierenden und nicht-terminierenden Programmenausführungen zu unterscheiden und modelliert nicht terminierende Programmausführungen akkurat.

Schließlich wurde die neue Kostenanalyse im Werkzeug CoFloCo implementiert und extensiv evaluiert. Die Evaluierung vergleicht CoFloCo mit anderen, dem aktuellen Stand der Forschung entsprechenden Tools anhand einer Vielzahl von Benchmarks. Diese Benchmarks bestehen aus imperativen und funktionalen Programmen sowie aus Termersetzungssystemen. CoFloCo zeigt durchgehend eine sehr gute Leistung in allen Kategorien und demonstriert damit die Leistungsfähigkeit und Vielseitigkeit der entwickelten Kostenanalyse.

German
URN: urn:nbn:de:tuda-tuprints-67465
Classification DDC: 000 Generalities, computers, information > 004 Computer science
Divisions: 20 Department of Computer Science > Theoretische Informatik
20 Department of Computer Science > Formal Methods in System Engineering
20 Department of Computer Science > Software Engineering
20 Department of Computer Science > Sprachtechnologie
Date Deposited: 04 Sep 2017 12:46