Stud.IP Uni Oldenburg
University of Oldenburg
27.11.2022 20:05:13
ThesisTopics

Personal details

Title Lokalität von Persistenter Linearizierbarkeit
Description
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.
Home institution Department of Computing Science
Type of work conceptual / theoretical
Type of thesis Bachelor's
Author Prof. Dr. Heike Wehrheim
Status assigned
Problem statement
Requirement
Created 01/06/22