[Back]


Doctor's Theses (authored and supervised):

R. Mittermayr:
"Kronecker Algebra Based Analysis of Shared Memory Concurrent Systems";
Supervisor, Reviewer: J. Blieberger, B. Burgstaller; E 183-1, 2016; oral examination: 2016-10-11.



English abstract:
Program analysis of multi-threaded software is still a challenge. Beside other reasons, this comes from the fact that synchronization has to be taken into account. In particular, a suitable graph based model has been missing. In this dissertation, we introduce a novel graph based approach. It is based on the idea that thread interleavings can be studied with a matrix calculus. This is a novel approach in this research area. Our sparse matrix representations of a program are manipulated using Kronecker algebra. In the course of this dissertation we extend it and prove some important properties. The underlying graph ¿ which we call concurrent program graph (CPG) ¿ represents a multi-threaded program and plays a similar role for concurrent systems as control flow graphs do for sequential programs. Thus a suitable graph model for program analysis of multi-threaded software is set up. Due to synchronization, e.g., via synchronization primitives like semaphores and barriers, it turns out that often only very small parts of the resulting graph are actually needed, whereas the rest is unreachable. A lazy implementation of matrix operations ensures that unreachable parts are never calculated. This speeds up processing significantly and shows that our approach is very promising. We parallelized this lazy algorithm and thus gain additional speedup by exploiting the power of modern multi-core architectures. In this dissertation, we will show how we use CPGs to detect deadlocks statically in concurrent programs. We present a new synchronization construct modeling barriers. By applying this, we are able to statically analyze Ada multi-tasking programs that employ barriers for synchronization issues. It turns out that our Kronecker algebra implementation can be used out-of-the-box for CPGs using such barrier synchronization primitives. In addition, we show that CPGs can be used as a basis for a worst-case execution time (WCET) analysis of multi-threaded programs. We employ a generating functions based approach for setting up data flow equations which are then solved by well-known elimination based data flow analysis methods. With this approach, we are able to calculate the WCET (including stalling times) of multi-threaded programs with a non-linear function solver. Non-linearity turns out to be inherent to the multi-threaded WCET problem. Finally, we show how our Kronecker algebra based approach can be adopted in the field of railway systems. For multiple trains in a railway disposition system and based on given routes, it can be used to suggest deadlock-free movements only. Additiona lconstraints, such as overtaking and train connections, may be taken into account. Our railway approach was already extended by others, e.g., to save energy by minimizing stop and go of trains.

German abstract:
Programmanalyse von nebenläufigen Programmen ist immer noch eine Herausforderung. Das kommt unter anderem daher, dass Synchronisation berücksichtigt werden muss. Im Speziellen fehlte bisher ein geeignetes Graphenmodell. Mit dieser Dissertation führen wir einen graphenbasierten Ansatz ein. Dieser fußt auf der Idee, dass zeitlich verschränkte Abarbeitung (thread interleavings) durch einen Matrizenkalkül betrachtet werden kann. Dies ist neu in diesem Forschungsgebiet. Die dünnbesetzten Matrizen eines Programmes werden mittels Kronecker Algebra-Operationen manipuliert. Im Zuge dieser Dissertation wird diese erweitert und manch wichtige Eigenschaft bewiesen. Der zugrundeliegende Graph, den wir concurrent program graph (CPG) nennen, repräsentiert ein nebenläufiges Programm und spielt eine ähnliche Rolle wie Kontrollflussgraphen für sequentielle Programme. Daher ist er ein geeignetes Modell für die Programmanalyse von nebenläufigen Programmen. Es stellt sich heraus, dass durch Synchronisation (z.B. durch Synchronisationsprimitive wie Semaphoren oder Barrieren) oft nur ein sehr kleiner Teil des resultierenden Graphen nötig und der Rest unerreichbar ist. Eine verzögerte (im Englischen oft als ¿lazy¿ bezeichnete) Auswertung der Matrixoperationen stellt sicher, dass unerreichbare Teile nie berechnet werden. Das beschleunigt die Berechnung signifikant und zeigt, dass unser Ansatz vielversprechend ist. Die Parallelisierung dieses Algorithmus für Mehrkern-Architekturen ermöglichte eine signifikante Laufzeit-Reduktion. In dieser Dissertation zeigen wir, wie CPGs zum statischen Finden von Deadlocks in nebenläufigen Programmen verwendet werden können. Des Weiteren führen wir ein neues Synchronisationskonstrukt, das Barrieren modelliert, ein. Dieses Konstrukt ermöglicht die statische Analyse von nebenläufigen Ada-Programmen, die Barrieren zur Synchronisation verwenden. Programme, die auf diese Synchronisationsprimitive bauen, können mit unserer völlig unveränderten Kronecker Algebra-Implementierung analysiert werden. Zusätzlich zeigen wir, dass CPGs als Basis für eine Analyse der maximalen Laufzeit ¿ im Englischen oft als worst-case execution time (WCET) bezeichnet ¿ verwendet werden können. Wir verwenden einen Ansatz, der auf erzeugende Funktionen basiert. Datenflussgleichungen werden durch etablierte (sogenannte elimination based ) Datenflussanalysemethoden gelöst. Mit diesem Ansatz wird es möglich, die WCET von nebenläufigen Programmen zu berechnen. Diese WCET inkludiert auch Zeiten, in denen Threads blockiert sind. Mittels eines nicht-linearen Funktionslöser werden die Gleichungen gelöst. Es zeigt sich, dass nebenläufigen WCET-Problemen Nicht-Linearität inhärent ist. Schließlich zeigen wir, wie unser Kronecker Algebra-Ansatz im Bereich der Eisenbahn verwendet werden kann. Bei gegebenen Fahrstraßen wird es dadurch Dispositionssystemen möglich, für mehrere Züge automatisch deadlockfreie Zugbewegungen vorzuschlagen. Zusätzliche Bedingungen, wie z.B. Überholungen und Zugverbindungen, können dabei beachtet werden. Dieser Ansatz wurde bereits von anderen erweitert, um z.B. durch Minimierung von Brems-/Beschleunigungszyklen energiesparend zu fahren.

Keywords:
Kroencker Algebra, Shared Memory Concurrent Systems, WCET


Electronic version of the publication:
http://publik.tuwien.ac.at/files/PubDat_251739.pdf


Created from the Publication Database of the Vienna University of Technology.