Flores Montoya, Antonio (2017)
Cost Analysis of Programs Based on the Refinement of Cost Relations.
Technische Universität Darmstadt
Dissertation, Erstveröffentlichung
Kurzbeschreibung (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.
Typ des Eintrags: | Dissertation | ||||
---|---|---|---|---|---|
Erschienen: | 2017 | ||||
Autor(en): | Flores Montoya, Antonio | ||||
Art des Eintrags: | Erstveröffentlichung | ||||
Titel: | Cost Analysis of Programs Based on the Refinement of Cost Relations | ||||
Sprache: | Englisch | ||||
Referenten: | Hähnle, Prof. Dr. Reiner ; Giesl, Prof. Dr. Jürgen | ||||
Publikationsjahr: | 28 August 2017 | ||||
Ort: | Darmstadt | ||||
Datum der mündlichen Prüfung: | 14 Juli 2017 | ||||
URL / URN: | http://tuprints.ulb.tu-darmstadt.de/6746 | ||||
Kurzbeschreibung (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. |
||||
Alternatives oder übersetztes Abstract: |
|
||||
URN: | urn:nbn:de:tuda-tuprints-67465 | ||||
Sachgruppe der Dewey Dezimalklassifikatin (DDC): | 000 Allgemeines, Informatik, Informationswissenschaft > 004 Informatik | ||||
Fachbereich(e)/-gebiet(e): | 20 Fachbereich Informatik > Theoretische Informatik 20 Fachbereich Informatik > Formal Methods in System Engineering 20 Fachbereich Informatik > Software Engineering 20 Fachbereich Informatik > Sprachtechnologie 20 Fachbereich Informatik |
||||
Hinterlegungsdatum: | 10 Sep 2017 19:55 | ||||
Letzte Änderung: | 10 Sep 2017 19:55 | ||||
PPN: | |||||
Referenten: | Hähnle, Prof. Dr. Reiner ; Giesl, Prof. Dr. Jürgen | ||||
Datum der mündlichen Prüfung / Verteidigung / mdl. Prüfung: | 14 Juli 2017 | ||||
Export: | |||||
Suche nach Titel in: | TUfind oder in Google |
Frage zum Eintrag |
Optionen (nur für Redakteure)
Redaktionelle Details anzeigen |