Lina4WM Linearizierbarkeitsbeweise für schwache Speichermodelle

• Antragstellerin: Professorin Dr. Heike Wehrheim
• Fachliche Zuordnung: Softwaretechnik und Programmiersprachen
• Förderung: Förderung von 2010 bis 2018
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 163003744

Parallele Programme werden heutzutage meist tatsächlich auf Mehrkernrechnern und damit echt parallel ausgeführt. Bezüglich der Performance paralleler Programme bringt dies erhebliche Gewinne. Doch ist damit aber auch ein erhebliches Risiko verbunden: die Speichermodelle von Mehrkernrechnern sind deutlich schwächer als die normalerweise angenommenen sequentiell konsistenten Speichermodelle. Dies führt zu unerwarteten Ausführungen paralleler Programme und letztendlich zu Fehlern. Das Projekt Lina4WM beschäftigt sich mit der Korrektheit einer bestimmten Klasse von parallelen Programmen unter der Annahme schwacher Speichermodelle. Die Programmklasse sind sogenannte Parallele Datenstrukturen, das heißt Algorithmen, die einen parallelen Zugriff auf Datenstrukturen wie Keller, Schlangen oder Hashtabellen ermöglichen. Solche Datenstrukturen sind hochoptimiert für Parallelität und lassen insbesondere auch Dataraces zu. Sie sind damit besonders anfällig für die Effekte schwacher Speichermodelle. Das Projekt soll eine Beweismethodik für die Korrektheit paralleler Datenstrukturen auf schwachen Speichermodellen entwickeln. Das zentrale Korrektheitskriterium für parallele Datenstrukturen ist Linearizierbarkeit. Die Basis für die Beweismethodik werden maschinengestützte Simulationsbeweise sein. Das Projekt arbeitet also insgesamt an der Erarbeitung von Simulationsbeweisen für Linearizierbarkeit von parallelen Datenstrukturen auf schwachen Speichermodellen.

• DFG-Verfahren: Sachbeihilfen