Automated complexity analysis of rewrite systems

Frohn, Florian; Giesl, Jürgen; Genaim, Samir

doi:37820

Automated complexity analysis of rewrite systems = Automatische Komplexitätsanalyse von Reduktionssystemen

Frohn, Florian^RWTH*

2018 & 2019

Verantwortlichkeitsangabevorgelegt von Florian Frohn, Master of Science

ImpressumAachen 2018

Umfang1 Online-Ressource (282 Seiten) : Illustrationen

Dissertation, RWTH Aachen University, 2018

Veröffentlicht auf dem Publikationsserver der RWTH Aachen University 2019

Genehmigende Fakultät
Fak01

Hauptberichter/Gutachter
Giesl, Jürgen (Thesis advisor)^RWTH* ; Genaim, Samir (Thesis advisor)

Tag der mündlichen Prüfung/Habilitation
2018-12-11

Online
DOI: 10.18154/RWTH-2018-231555
URL: http://publications.rwth-aachen.de/record/751705/files/751705.pdf

Einrichtungen

Inhaltliche Beschreibung (Schlagwörter)
Integer-Transitionssysteme (frei) ; Komplexitätsanalysse (frei) ; Termersetzung (frei) ; Verifikation (frei)

Thematische Einordnung (Klassifikation)
DDC: 004

Kurzfassung
Neben Korrektheit ist Effizienz eine der wichtigsten Voraussetzungen für den Erfolg von Software: Das gesuchte Ergebnis muss nicht nur korrekt, sondern auch rechtzeitig berechnet werden. Deshalb ist es in der Praxis unverzichtbar, die Laufzeitkomplexität von Software zu analysieren. Allerdings ist es unpraktikabel, die Komplexität von Programmen manuell zu analysieren. Folglich werden automatische Techniken benötigt. So können Performance-Probleme genauso automatisiert gefunden werden wie andere Fehler, die von Tools zur statischen Analyse erkannt werden. Jedoch bringt es etliche Probleme mit sich, die Komplexität realistischer Programme statisch zu analysieren. Zum Beispiel haben die meisten Programmiersprachen keine formale Semantik. Zudem unterscheiden sich verschiedene Sprachen mitunter stark, sodass statische Analysen für eine Sprache oft nicht auf andere übertragbar sind. Eine verbreitete Lösung ist, Programme in Reduktionssysteme, insbesondere Term- oder Integer-Ersetzungssysteme, zu übersetzen und deren Komplexität zu analysieren. Leider haben aktuelle Techniken zur Analyse von Reduktionssystemen zahlreiche Einschränkungen. Zunächst sind die meisten Techniken auf die Inferenz oberer Schranken für die Worst-Case-Komplexität beschränkt. Außerdem können aktuelle Tools ihre Stärken nur unter der Annahme einer strikten Auswertungsstrategie voll ausspielen. Schließlich unterstützenviele Techniken für Integer-Ersetzung ausschließlich Endrekursion. Diese Arbeit überwindet die genannten Limitierungen teilweise. Sie stellt unter anderem die ersten Techniken zur Inferenz unterer Schranken für die Worst-Case-Komplexität vor. Eine wichtige Anwendung für solche Schranken ist das Finden von Denial-of-Service-Angriffsmöglichkeiten, die entstehen, wenn die Laufzeit eines Programms größer ist als erwartet. Bezüglich oberer Schranken zeigt diese Arbeit, wie Techniken für Termersetzung, die eine strikte Auswertungsstrategie erfordern, genutzt werden können, ohne eine bestimmte Strategie vorauszusetzen. Ebenso zeigt sie, wie Techniken für Integer-Ersetzung, die auf Endrekursion eingeschränkt sind, auch für nicht endrekursive Systeme genutzt werden können. Somit können Übersetzungen in Reduktionssysteme nun für ausdrucksstärkere Klassen von Programmen und neue Anwendungsfälle eingesetzt werden, z.B. die Erkennung von Denial-of-Service-Angriffsmöglichkeiten. Dies gilt insbesondere für Programme, die auf Integern oder baumförmigen Datenstrukturen arbeiten, da sich diese auf natürliche Art und Weise in Integer- bzw. Termersetzung übersetzen lassen. Folglich deckt diese Arbeit große Teile der Features realistischer Programmiersprachen ab. Die präsentierten Techniken wurden in den Tools AProVE und LoAT implementiert, die die Komplexität von Reduktionssystemen vollautomatisch analysieren können. Ausführliche Experimente demonstrieren ihre praktische Anwendbarkeit.

Besides functional correctness, one of the most important prerequisites for the success of a piece of software is efficiency: The desired results need to be computed not only correctly, but also in time. Thus, analyzing the runtime complexity of software is indispensable in practice. On the other hand, analyzing the complexity of large programs manually is infeasible. Hence, automated complexity analysis techniques are needed. In this way, performance pitfalls can be highlighted automatically like other bugs which can nowadays be found by compilers or static analyzers. However, statically analyzing the complexity of real-world programs poses several problems. For example, most programming languages lack formal semantics. Moreover, different programming languages offer different features, so static analyses for one language do not necessarily apply to others. A common solution for these problems is to transform programs into low-level formalisms like term or integer rewrite systems that can be analyzed without worrying about language-specific peculiarities. Unfortunately, state-of-the-art complexity analysis techniques for rewrite systems have several limitations. Firstly, most of them are restricted to the inference of upper bounds on the worst-case complexity. Moreover, existing complexity analyzers only reach their full potential if an eager evaluation strategy is fixed, which is sometimes undesired in practice. Finally, many techniques for integer rewriting just support tail recursion. This thesis partially overcomes these limitations. To this end, the first techniques for the inference of lower bounds on the worst-case complexity are introduced. One important use case of such lower bounds is to witness denial-of-service vulnerabilities (whose absence can be proven via upper bounds), which arise if the runtime of a program exceeds expectations. Regarding upper bounds, this thesis shows how complexity analysis techniques for term rewriting which require an eager evaluation strategy can also be used without assuming eager evaluation. Similarly, it shows how complexity analysis techniques for integer rewriting which are restricted to tail recursion can also be used to analyze non-tail-recursive systems. Consequently, complexity-preserving transformations to rewrite systems can now be used for more applications - like the detection of denial-of-service vulnerabilities - and richer classes of programs. This is true for both programs operating on integers as well as programs operating on tree-shaped data, which can naturally be transformed to integer and term rewrite systems, respectively. Hence, this thesis covers a large subset of the features provided by real-world programming languages. The presented techniques were implemented in the tools AProVE and LoAT, which can analyze the complexity of rewrite systems fully automatically. Extensive experiments demonstrate the feasibility of the presented techniques in practice.

OpenAccess:
PDF
(additional files)