Softwareentwicklungspraktikum (SEP): Verifizierte C-Library für lockfreie Datenstrukturen
Sommersemester 2023
News
- 2. Feb
-
Die Informationen auf der Projektseite sind noch vorläufig. - 11. Apr
- Das Kickoff-Meeting findet am Montag, den 17. April, um 10:00 Uhr, IZ 358 statt.
Überblick
Das diesjährige Softwareentwicklungsprojekt des Instituts für Theoretische Informatik (TCS) beschäftigt sich mit der Entwicklung und Verifikation nebenläufiger Datenstrukturen. Genauer soll eine C-Library sogennanter "lockfreier Datenstrukturen" entwickelt und mit Hilfe unseres Verifikationstools Dartagnan verifiziert und optimiert werden. Die Besonderheit von nebenläufigen Datenstrukturen und allgemein nebenläufigen Programmen ist, dass ihr Verhalten subtil abhängig ist von sowohl der verwendeten Programmiersprache als auch der Prozessorarchitektur auf der sie ausgeführt werden. Es wird drei Arbeitsgruppen geben: Gruppe (1) entwickelt die Datenstrukturen und Gruppe (2) entwickelt Locking Algorithmen und Gruppe (3) verifiziert und optimiert die entwickelten Datenstrukturen und Locking Algorithmen.
Motivation
Bei der Entwicklung sicherheitskritischer Software und Software für den Finanzsektor wird besonderes Augenmerk auf die Qualitätssicherung gelegt, da Fehler (Bugs) hier zu schweren Personen- und Sachschäden führen können. Ein großes Problem bei der Qualitätssicherung stellt allerdings die Komplexität heutiger Computersysteme dar. Programme werden in Hochsprachen geschrieben, danach zu Assembler-Code kompiliert und letztendlich auf Prozessoren ausgeführt. Dabei führen sowohl der Compiler der Hochsprache als auch die Prozessoren selber viele Optimierungen durch, die das Verhalten des Programms beeinflussen. Dies kann zu unerwarteten Bugs führen, wenn der Programmierer diese Optimierungen nicht berücksichtigt. Eine Möglichkeit mit diesem Problem umzugehen, ist es die Compileroptimierungen auszustellen und sogenannte "Barriers" im Code zu platzieren, um die Optimierungen des Prozessors ebenfalls zu limitieren. Dies führt zwar zu korrektem, aber sehr ineffizientem Code.
Im diesjährigen SEP wollen wir zum einen eine C-Library von lockfreien Datenstrukturen und eine C-Library mit Locking Primitives entwickeln. Die Libraries sollen trotz aller Optimierungen korrekt funktioneren und diese sogar ausnutzen, um effizient zu sein. Wir wollen desweiteren die Benutzer unserer Library und auch uns selber davon überzeugen können, dass diese Bug-frei ist. Dazu wollen wir das Verifikationstool Dartagnan verwenden, um Bugs zu finden und zu beheben. Desweiteren wollen wir die Effizienz unserer Datenstrukturen maximieren, indem wir nur wirklich notwendige Barriers verwenden. Auch hier kann Dartagnan genutzt werden, um überflüssige Barriers zu identifizieren und zu optimieren.
Die Entwicklung der beiden Libraries und die Verifikation/Optimierung dieser werden wir in drei Arbeitsgruppen aufteilen.
Betreuer
Betreut wird das Projekt durch Roland Meyer, Thomas Haas, Sören van der Wall und Jan Grünke. Ansprechpartner sind Thomas Haas, Sören van der Wall und Jan Grünke.