Automated amortised analysis [Elektronische Ressource] / vorgelegt von Steffen Jost

Steffen Jost

Sujets

• Informatik

Informations

• Publié par: ludwig-maximilians-universitat_munchen
• Publié le: 01 janvier 2010
• Nombre de lectures: 48
• Langue: Deutsch
• Poids de l'ouvrage: 1 Mo

Extrait

Automated Amortised Analysis
Dissertation an der Fakult at
fur Mathematik, Informatik und Statistik
der Ludwig-Maximilians-Universit at Munc hen
Vorgelegt von
Dipl.-Math. Ste en Jost
am 9. August 2010Berichterstatter:
Prof. Martin Hofmann
(Ludwig-Maximilians-Universit at Munc hen, Deutschland)
Prof. Kevin Hammond
(University of St Andrews, Schottland)
Tag der mundlic hen Prufung:
16. September 2010
iiTo my grand-parents, who could not a ord to wait for this thesis to be completed.
vDeutsche Zusammenfassung
Ste en Jost stellt eine neuartige statische Programmanalyse vor, welche vollautoma-
tisch Schranken an den Verbrauch quantitativer Ressourcen berechnet. Die Grun-
didee basiert auf der Technik der Amortisierten Komplexitatsanalyse, deren nicht-
triviale Automatisierung durch ein erweitertes Typsystem erreicht wird. Das Typsys-
tem berechnet als Nebenprodukt ein lineares Gleichungssystem, dessen Losungen
Koe zienten f ur lineare Formeln liefern. Diese Formeln stellen garantierte obere
Schranken an den Speicher- oder Zeitverbrauch des analysierten Programms dar, in
Abhangigkeit von den verschiedenen Eingabegro en des Programms. Die Relevanz
der einzelnen Eingabegro en auf den Ressourcenverbrauch wird so deutlich bezi ert.
Die formale Korrektheit der Analyse wird fur eine funktionale Programmiersprache
bewiesen. Die strikte Sprache erlaubt: Typen hoherer Ordnung, volle Rekursion, ver-
schachtelte Datentypen, explizites Aufschieben der Auswertung und Aliasing. Die
formale Beschreibung der Analyse befasst sich primar mit dem Verbrauch von dy-
namischen Speicherplatz. Fur eine Reihe von realistischen Programmbeispielen wird
demonstriert, dass die angefertigte generische Implementation auch gute Schranken
an den Verbrauch von Stapelspeicher und der maximalen Ausfuhrungszeit ermitteln
kann. Die Analyse ist sehr e zient implementierbar, und behandelt auch gr o ere
Beispielprogramme vollstandig in wenigen Sekunden.
viEnglish Abstract
Ste en Jost researched a novel static program analysis that automatically infers for-
mally guaranteed upper bounds on the use of compositional quantitative resources.
The technique is based on the manual amortised complexity analysis. Inference is
achieved through a type system annotated with linear constraints. Any solution to
the collected constraints yields the coe cients of a formula, that expresses an upper
bound on the resource consumption of a program through the sizes of its various
inputs.
The main result is the formal soundness proof of the proposed analysis for a functional
language. The strictly evaluated language features higher-order types, full mutual
recursion, nested data types, suspension of evaluation, and can deal with aliased data.
The presentation focuses on heap space bounds. Extensions allowing the inference
of bounds on stack space usage and worst-case execution time are demonstrated
for several realistic program examples. These bounds were inferred by the created
generic implementation of the technique. The implementation is highly e cient, and
solves even large examples within seconds.
viiAcknowledgements
The rst person to thank here is my supervisor Martin Hofmann. He kindly invited
me to write this thesis about automatic resource analysis at his chair in theoretical
computer science in Munich. Martin provided me with essential guidance throughout,
especially whenever I believed the problems to be insurmountable.
I thank my current supervisor Kevin Hammond for his o er to work in St Andrews.
He provided me with manifold advice, valuable academic freedom and generous sup-
port to continue the research on my thesis while I worked for him in bonnie Scotland.
The members of the EmBounded and MRG research projects provided a highly
useful environment for researching this thesis. This allowed the analysis to reach an
unhoped-for maturity. I especially thank my colleague Hans-Wolfgang Loidl not only
for good remarks on my draft, but also for the excellent cooperation in producing and
maintaining the implementation and numerous program examples to be analysed.
Apologies to Brian Campbell for not providing him with a nal version of this thesis in
time, despite his dissertation extending this one. His comments on my dry technical
drafts and discussions on our respective works have been bene cial.
My friend and colleague Hugo Simoes deserves a similar apology. Discussing our
closely related works has always been interesting and led to signi cant improvements
of this thesis. Especially his observation, that preservation of memory consistency
for the higher-order system can be proven independently, came at a crucial point in
time.
My thanks extend to Pedro Vasconcelos for good discussions and for explaining
his good work on sized types to me; Olha Shkaravska for recognising the connec-
tion between Tarjan’s work and mine; Jeremy Siek, Ekaterina Komendantskaya and
Vladimir Komendantsky for discussions on co-induction; Graham Hutton for sug-
gesting to analyse his synthesised abstract machine; Christoph Herrmann and Robert
Rothenberg for proof reading.
I am grateful to my entire family for their ample support. I owe my wife Andrea
so much for taking care about really everything so that I could work on this thesis,
especially for such a long time. I thank her and our children Melina and Jannis for
still loving me despite all the weekends that I spent at my desk instead of with them.
Financial support is acknowledged from the Graduiertenkolleg Logik in der Informatik
Munich (GKLI); the EU FET-IST projects IST-510255 (EmBounded), IST-2001-
33149 (MRG), IST-248828 (Advance); and EPSRC grant EP/F030657/1 (Islay).
ix