Linearizierbarkeit ist ein Korrektheitkriterium für nebenläufige Datenstrukturen wie Keller oder Schlangen. Linearizierbarkeit garantiert, dass sich eine parallel genutzte Datenstruktur immer so verhält, als würde sie ihre Operationen atomar, sequentiell, eine nach der anderen ausführen. Eine wichtige Eigenschaft von Linearizierbarkeit ist Lokalität: wenn Datenstrukturen alleine linearizierbar sind, dann auch immer die gemeinsame Nutzung mehrerer Datenstrukturen.
Seit kurzem gibt es eine Erweiterung von Linearizierbarkeit, die bei persistentem Speicher Anwendung findet. Persistenter oder auch non-volatiler Speicher ist eine neue Speichertechnologie, bei der Daten im Hauptspeicher auch bei einem Systemcrash nicht verloren gehen. Für Persistente Linearizierbarkeit (oder auch englisch durable linearizability) und eine Abschwächung davon (buffered durable linearizability) ist bekannt, dass sie lokal bzw. nicht lokal ist; ein formaler Beweis fehlt aber bisher.
Die Aufgabe der Arbeit liegt nun darin, (a) solche existierenden Korrektheitskriterien formal in einem einheitlichen Rahmen zu definieren, sowie (b) für jede der Kriterien einen Beweis der Lokalität oder ein Gegenbeispiel anzugeben.

Literatur:
[1] Herlihy, Wing: Linearizability: A correctness condition for concurrent objects, ACM TOPLAS, Vol.12, No.3, 1990.
[2] Israelevitz, Mendes, Scott: Linearizability of persistent memory objects under a full-system-crash failure model, in: DISC 2016.