Robustness against Relaxed Memory Models
This web page accompanies our research project R2M2.
Summary (english)
For performance reasons, modern multiprocessors implement relaxed memory models that admit out-of-program-order and non-store atomic executions. While data race free programs are not sensitive to these relaxations, they pose a serious problem to the development of the underlying concurrency libraries. Routines that work correctly under sequential consistency show undesirable effects when run on relaxed memory models. Mutual exclusion algorithms, for example, fail if the program-order is relaxed only slightly. We say that these programs are not robust against the relaxations that the processor supports. To enforce robustness, the programmer has to add safety net instructions to the code that control the hardware - a task that has proven to be difficult, even for experts. With the widespread use of multi- processors, concurrency libraries become increasingly important in everyday programming and robustness is starting to be a key concern.
We propose to develop algorithms that check and enforce robustness of programs against relaxed memory models. Assuming a memory model and given a program, our procedures decide whether the relaxed behaviour coincides with the sequential consistency semantics. If this is not the case, they synthesize safety net instructions that enforce robust- ness. When built into a compiler, our algorithms thus hide the relaxed memory model from the programmer and provide the illusion of sequential consistency.
Checking robustness is challenging due to two sources of unboundedness in the problem. First, to ensure the analysis is independent from architectural parameters (like the size of write buffers), we cannot assume a bound on the program-order relaxations. Second, and with a similar argument, we cannot assume a bound on the number of clients to a library - although this number is finite in actual processors.
The project strives for theoretical as well as practical contributions to robustness analysis. From a theoretical point of view, our goal is to develop a proof method for computability and complexity results about robustness. The idea is to combine combinatorial reasoning about relaxed computations with language-theoretic methods. Developing such a general theory is well justified. Future processor generations will come with new memory models, and the techniques we develop here should carry over to these architectures. Indeed, our second goal is to apply the proof method in practice. We address robustness against the popular POWER processors that have a highly relaxed memory model. Moreover, we study robustness for concurrency libraries that act in an unknown environment.
To sum up, the central goals of our project are the following.
- Investigate combinatorial properties of computations that violate robustness.
- Based on this, develop language-theoretic techniques to decide robustness.
- Apply the method to check robustness against POWER processors.
- Extend the method to check robustness of concurrency libraries.
Summary (german)
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:
- Studium der kombinatorischen Eigenschaften Robustheit-verletzender Berechnungen.
- Basierend auf den Ergebnissen, Entwicklung sprachtheoretischer Verfahren zum Entscheiden von Robustheit.
- Anwendung zur Prüfung von Robustheit gegenüber POWER-Prozessoren.
- Erweiterung der Methode zur Prüfung von Robustheit von Concurrency-Bibliotheken.
Keywords
- Keywords (in German):
- Schwache Speichermodelle, Robustheit, Verifikation, Entscheidbarkeit und Komplexität, Nebenläufigkeitstheorie.
- Keywords (in English):
- Relaxed Memory Models, Robustness, Verification, Decidability and Complexity, Concurrency Theory.