Tief reichendes Parallelismus

Viele berechnungsintensive Probleme erfordern die Struktur-Analyse von großen Graphen, die beispielsweise soziale Netzwerke, Computernetzwerke oder das Verhalten von digitalen System (Model Checking)repräsentieren. NeueProzessorarchitekturen priorisieren allerdings erweiterte Nebenläufigkeit anstelle von sequenzieller Ausführungsgeschwindigkeit. Das führt dazu, dass die Skalierbarkeit von aktuellen Graphalgorithmen auf neuesten Prozessoren ein Ende gefunden hat und keinen Gebrauch von diesem exponentiellen Wachstum der Nebenläufigkeit macht. Ich werde dieses Problem angehen, indem ich meinen Fokus auf eine fundamentale Gruppe von Graphen-Analyse-Algorithmen lege. Der wichtigste Bestandteil vieler Graphenalgorithmen ist die so genannte Tiefensuche ("depth-first search", DFS). Die Ergebnisse bereits vieler Wissenschaftler Untersuchungen, inklusive meine eigene, bestätigen, dass bestimmte, DFS-basierte Algorithmen parallelisiert werden können. Um diese Ergebnissen zu verallgemeinern, präsentiert dieser Projektvorschlag eine Strategie, die viele wichtige Graphenalgorithmen parallelisieren kann und dazu theoretische Grundlagen bereit stellt. Das vorgeschlagene Projekt ist geteilt in zwei komplementäre Ansätze: Im Teil (A), wird formale DFS Charakterisierungen angestellt um die parallelen DFS Algorithmen aus früheren Arbeiten zu beschreiben. Dies wird die notwendigen Voraussetzungen schaffen, um in vielen Algorithmen, die verschiedene Graphenanalysen durchführen, DFS durch eine parallele DFS zu ersetzen, zum Beispiel. Die Komplexität paralleler Algorithmen macht deren manuelle Verifikation praktisch unmöglich. Aktuelle automatisierte Methoden (wie zum Beispiel vollständiges Model Checking) sind noch nicht kräftig genug, um die notwendigen Invarianten für Graphenalgorithmen zu liefern. Deswegen werden in Teil (B) die Benutzung von Lemmata aus meinen handgeschriebenen Beweisen für DFS Algorithmen kombiniert mit kräftige Model Checking Algorithmen zum Finden von Invarianten zu ermöglichen. Diese Arbeit wird die erste Verifikationsmethode liefern, die mit (Zustandsunendlichen) Graphenalgorithmen umgehen kann. Teil (A) und (B) ergänzen sich: Neue parallele Algorithmen stellen Model Checking Programme vor interessante Aufgaben, während bessere Verifikationsmethoden mit komplexeren parallelen Algorithmen umgehen können. Außerdem kann Model Checking selbst parallelisiert werden, da DFS dort auch viel verwendet wird. Durch meine Erfahrung als Hauptentwickler der Model Checker VVT und LTSmin habe ich eine solide Grundlage um solche neuen parallelen Algorithmen zu evaluieren und die Ergebnisse zu veröffentlichen. Die FORSYTE Abteilung an der TU Wien war und wird ein inspirierender Gastgeber bleiben, bei dem ich meine Erfahrungen anwenden kann, auf die vielen Tools die dort Entwickelt werden. Des weiteren wird es viele Synergieeffekte durch die einmalige, international bekannte Position, die FORSYTE innerhalb des Österreichischen "Rigorous Systems Engineering" Konsortiums spielt, geben.