TP-L: Semantik und Verifikation von parallelen Systemen
Um von der Leistungssteigerung moderner Prozessoren zu profitieren, müssen Softwareanwendungen parallel ausgeführt werden können und mit der Anzahl der verfügbaren Prozessorkerne skalieren. Allerdings sind viele Softwareanwendungen über Jahre gewachsen und daher überwiegend sequentiell implementiert. Da in den vorhandenen Softwareanwendungen viel Geschäftsexpertise steckt, ist eine Parallelisierung der vorhandenen Software einer vollständigen Neuimplementierung vorzuziehen.
Prinzipiell können während des Parallelisierungsprozesses menschliche Fehler in der manuellen oder semi-automtischen Parallelisierung sowie unvollständige Informationen während der Parallelisierung zu Verhaltensänderungen des parallelisierten Programms führen. Daher muss geprüft werden, ob das parallelisierte Programm weiterhin funktional korrekt ist. In parallelen Programmen zeigt sich Fehlerverhalten unter Umständen nur in selten auftreten Ausführungen. Daher eignet sich Verifikation besonders gut zur Absicherung der funktionalen Korrektheit. Allerdings scheitert der Einsatz von Verifikation häufig bereits daran, dass keine formale Spezifikation des funktionalen Verhaltens existiert. Für parallelisierte Programme dagegen kann das sequentielle Ursprungsprogramm als Spezifikation dienen.
Ziel des Teilprojekts L ist es daher, die funktionale Äquivalenz zwischen sequentiellem und parallelisiertem Programm zu prüfen. Wie im linken Teil der nachfolgende Grafik beschrieben, muss dafür geprüft werden, ob das sequentielle und das parallelisierte Programm bei gleicher Eingabe die gleiche Ausgabe berechnen. Im Folgenden werden die Herausforderung dieser Prüfung und unser Lösungsansatz beschrieben.
Die Herausforderung für Teilprojekt L ist die Vielzahl von parallelen Programmausführungen für die Äquivalenzprüfung beherrschbar zu machen. Erschwerend kommt hinzu, dass moderne Multiprozessoren schwächere Konsistenzgarantien als sequentielle Konsistenz bieten und sich dadurch die Anzahl an möglichen, parallelen Ausführungen zusätzlich erhöht. Um diese Herausforderung trotzdem zu meistern, wird die Äquivalenzprüfung in folgende drei Teilprüfungen dekomponiert, die es erlaubt lediglich die letzte Teilprüfung zu wiederholen, wenn sich die Konsistenzgarantien des Speichermodells ändern.
- Partielle Äquivalenz: unter Annahme von sequentieller Konsistenz prüfen, ob das sequentielle und das parallelisierte Programm bei gleicher Eingabe die gleiche Ausgabe berechnen, wenn beide terminieren
- Terminierung: unter Annahme von sequentieller Konsistenz nachweisen, dass das parallelisierte Programm für alle Eingaben terminiert, das heißt z.B. kein Deadlock existiert, alle Schleifen terminieren, etc.
- Garantie von ausschließlich sequentiellem konsistentem Verhalten:
- durch Nachweis von sequentieller Konsistenz trotz Ausführung auf einem schwächeren Speichermodell oder
- durch die Ergreifung von Maßnahmen zur Wiederherstellung von sequentieller Konsistenz
Weiterhin sollen Parallelisierungsmuster dazu genutzt werden, um
- obige Prüfungen in weitere Teilprüfungen zu unterteilen,
- gewisse Teilaspekte einmalig für eine Klasse von Programmen zu prüfen oder
- die geeignetste Methode für eine Teilprüfung auszuwählen.