Robustheit gegenüber schwachen Speichermodellen

• Antragsteller: Professor Dr. Roland Meyer
• Fachliche Zuordnung: Theoretische Informatik ; Rechnerarchitektur, eingebettete und massiv parallele Systeme
• Förderung: Förderung von 2013 bis 2017
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 241337241

Multiprozessoren realisieren schwache Speichermodelle, die von der Programmordnung abweichende sowie nicht~atomare Ausführungen unterstützen. Während Data~Race~freie Programme gegenüber solchen Optimierungen unempfindlich sind, stellen sie für die Entwicklung der zugrundeliegenden Concurrency~Bibliotheken ein Problem dar. Verfahren, die unter sequentieller Konsistenz korrekt arbeiten, zeigen auf schwachen Speichern unerwünschte Effekte. Diese fehlerhaften Programme sind nicht robust gegenüber dem Speichermodell. Um Robustheit zu garantieren, muss die Programmiererin zusätzliche Safety~Net~Befehle in das Programm einfügen, die den Prozessor kontrollieren ~ eine selbst für Experten schwierige Aufgabe. Mit der zunehmenden Verbreitung von Multiprozessoren werden Concurrency~Bibliotheken in der alltäglichen Programmierung immer wichtiger, und Robustheit wird zu einem Kernanliegen. In diesem Projekt werden Algorithmen entwickelt, die automatisch die Robustheit eines Programms gegenüber einem Speichermodell prüfen und, falls nötig, erzwingen. Angenommen ein Speichermodell und gegeben ein Programm entscheiden die Verfahren, ob das Verhalten des Programms unter dem Speichermodell mit der sequentiell~konsistenten Semantik übereinstimmt. Ist das nicht der Fall, werden Safety~Net~Befehle berechnet, die Robustheit garantieren. Das Verfahren versteckt also das schwache Speichermodell vor dem Programmierer und erzeugt die Illusion sequentieller Konsistenz.Robustheit ist anspruchsvoll, da das Problem in zwei Dimensionen unbeschränkt ist. Um die Analyse von Parametern der Architektur (wie der Länge von Schreibpuffern) unabhängig zu halten, darf die Menge der Befehlsänderungen nicht eingeschränkt werden. Ferner kann keine Schranke für die Anzahl der Clients einer Bibliothek angenommen werden.Das Projekt strebt theoretische sowie praktische Beiträge zur Robustheitsanalyse an.Das theoretische Ziel ist die Entwicklung einer Beweismethode für Entscheidbarkeits~ und Komplexitätsresultate über Robustheit. Der Ansatz verbindet kombinatorische Argumente über schwache Berechnungen mit sprachtheoretischen Methoden. Die Entwicklung einer solch allgemeinen Theorie ist angebracht: sie sollte sich auch auf zukünftige Prozessorgenerationen übertragen lassen. Entsprechend ist die Anwendung der Beweismethode das zweite Ziel. Es wird Robustheit gegenüber den beliebten POWER~Prozessoren studiert, die ein sehr schwaches Speichermodell realisieren. Außerdem wird Robustheit von Concurrency~Bibliotheken angegangen, die in einer unbekannten Umgebung agieren.Zusammenfassend ergeben sich folgende Ziele:1. Studium der kombinatorischen Eigenschaften Robustheit~verletzender Berechnungen.2. Basierend auf den Ergebnissen, Entwicklung sprachtheoretischer Verfahren zumEntscheiden von Robustheit.3. Anwendung zur Prüfung von Robustheit gegenüber POWER~Prozessoren.4. Erweiterung der Methode zur Prüfung von Robustheit von Concurrency~Bibliotheken.

• DFG-Verfahren: Sachbeihilfen
• Internationaler Bezug: Frankreich
• Beteiligte Personen: Professor Dr. Ahmed Bouajjani; Professor Dr. Rupak Majumdar; Professor Dr. Arnd Poetzsch-Heffter; Professor Dr. Klaus Schneider