An execution trace verification method on linearizability [Elektronische Ressource] / Kristijan Dragičević

Sujets

• Naturwissenschaften

Informations

• Publié par: technische_universitat_munchen
• Publié le: 01 janvier 2011
• Nombre de lectures: 11
• Langue: Deutsch
• Poids de l'ouvrage: 1 Mo

Extrait

TECHNISCHE UNIVERSITAT MUNCHEN
Institut fur Informatik
Lehrstuhl fur Netzarchitekturen und Netzdienste
An Execution Trace Veri cation Method on
Linearizability
Kristijan Dragicevic
Vollstandiger Abdruck der von der Fakultat fur Informatik der Technischen
Universitat Munchen zur Erlangung des akademischen Grades eines
Doktors der Naturwissenschaften (Dr. rer. nat.)
genehmigten Dissertation.
Vorsitzender: Univ.-Prof. Dr. Helmut Seidl
Prufer der Dissertation: 1. Univ.-Prof. Dr. Georg Carle
2. Univ.-Prof. Dr. Marcel Waldvogel
Universitat Konstanz
Die Dissertation wurde am 24.01.2011 bei der Technischen Universitat Munchen
eingereicht und durch die Fakultat fur Informatik am 04.03.2011 angenommen. Ich versichere, dass ich die vorliegende Arbei selbstandig verfasst und nur die
angegebenen Quellen und Hilfsmittel verwendet habe.
I assure the single handed composition of this thesis only supported by declared
resources.
Garching, den 24. Januar 2011Kurzfassung:
Multicore Prozessoren sind inzwischen zur Standardarchitektur fur regulare
Prozessoren geworden. Folglich sind Programmierer immer mehr dazu ange-
halten, optimierte pa-rallele Software zu entwickeln. Die Verikation von par-
allelem Code ist sehr komplex, was neue praktikable Verikationsmethoden
notwendig macht. Es fehlt immer noch an Tools, welche komplexe parallele
Programme verizieren konnen. Diese Dissertation stellt eine Methode vor,
welche Ausfuhrungen von Programmen testet und zeigt, dass diese Methode
bereits wertvolle Resultate fur den Anwendungsprogrammierer liefert. Die Ve-
rikationsmethode wird verwendet um zu beweisen, dass ein Programm-Trace
linearisierbar ist. Daruberhinaus werden einige nutzliche allgemeine Eigen-
schaften von diversen Algorithmen herausgegri en, welche die praktische Re-
alisierung dieser Methode optimieren konnen. Ferner liefert diese Arbeit ein
Fallbeispiel anhand von Priority Queues um zu zeigen, wie diese Methode
angewendet werden kann. Das Fallbeispiel zeigt, dass praktikable Resultate
mithilfe dieser Methode erzeugt werden konnen.