VaST - Validierung von Software Transaktionalem Speicher

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

Software Transaktionaler Speicher (STM) ist ein Synchronisationsmechanismus für parallele Programme mit gemeinsamen Speicher. Für Programmierer bietet STM eine einfach zu nutzende Technik zur Kontrolle von Parallelität, die die Anwendung von expliziten Synchronisationstechniken wie Locks und Semaphoren überflüssig macht. Dazu muss der Programmierer Teile seines Codes als Transaktion definieren und das STM garantiert ihm dann die (scheinbar) atomare Ausführung dieses Programmteiles. Heutzutage gibt es eine Vielzahl von Vorschlägen für Transaktionalen Speicher, die TMs entweder in Hardware, in Software oder in einer Kombination beider (sogenannte hybride TMs) realisieren. TM Konzepte finden sich inzwischen in vielen etablierten Programmiersprachen und Prozessoren. Um eine hohe Performanz auch bei Tausenden von parallelen Prozessen zu erreichen, versuchen STMs möglichst viel Parallelität zu erlauben und beschränken Synchronisation auf das minimale Maß, das zur Erreichung von Korrektheit nötig ist. Korrektheit von STMs wird typischerweise durch den Begriff der Opakheit definiert, der die "scheinbar atomare" Ausführung der Transaktionen spezifiziert. Opakheit kann als eine Übertragung des Konzeptes der Serializierbarkeit aus dem Datenbankbereich auf Software Transaktionen angesehen werden; insbesondere wird dabei eine neue Anforderung für fehlschlagende Transaktionen eingeführt. Das wesentliche Ziel dieses Projektes ist die Entwicklung einer Methodensammlung für die Validierung von STMs. Diese wird drei Kernbestandteile beinhalten: (1) eine Methode (und ein Werkzeug) zum Testen von STMs, (2) eine Methode (und ein Werkzeug) zum Model Checking von STMs, und (3) eine Methode für mechanisierte Beweise der Korrektheit von STMs. Dadurch soll das Projekt die gesamte Entwurfsphase der STM Entwicklung unterstützen, vom schnellen Prototyping in frühen Entwurfsschritten hin zum Endprodukt eines hoch performanten, formal verifizierten STM Algorithmus.

• DFG-Verfahren: Sachbeihilfen