Forschung
Programmiersprachen und Tools Lab
Memory Fairness
Wie sollte eine unendliche Ausführung in einer Situation mit schwachem Speicher eingeschränkt werden? Wann wird ein nebenläufiges Programm in dieser Umgebung beendet? Fragen wie diese möchten wir mit unserem Projekt beantworten.
Lebendigkeitseigenschaften, wie z. B. die Beendigung, selbst der einfachsten konkurrierenden Programme mit gemeinsamem Speicher unter sequenzieller Konsistenz erfordern in der Regel einige Fairness-Annahmen über den Planer. Bei Modellen mit schwachem Speicher sind die Standardbegriffe der Thread-Fairness unzureichend, und eine zusätzliche Fairness-Eigenschaft, die Speicher-Fairness, wird benötigt. In diesem Projekt schlagen wir Definitionen für Speicher-Fairness im Rahmen operativer und deklarativer Speichermodelle wie SC, x86-TSO, RA und StrongCOH vor und untersuchen ihre Verwendung für die Modell- und Abbruchprüfung von nebenläufigen Programmen mit Synchronisation auf niedriger Ebene.