Verifikation Lock-freier Algorithmen

点击翻译按钮获取中文摘要

Durch die Einführung von Multicore-Architekturen ist in den letzten Jahren verstärkt die Notwendigkeit entstanden, parallele Algorithmen zu entwickeln und auf ihre Korrektheit zu untersuchen. Von besonderem Interesse sind dabei seit einiger Zeit Algorithmen, die nicht dem traditionellen Ansatz folgen, Locks oder Semaphore zu verwenden: Lock-freie Algorithmen arbeiten stattdessen mit Maschinen-Instruktionen wie CAS oder LL/SC, die neuerdings auch in Programmiersprachen wie Java oder C# angeboten werden. Die Anwendungen dieser Algorithmen reichen von der Verwaltung von Prozessqueues über Echtzeitspiele bis zu Hashtabellen für die Verwaltung von Indexstrukturen in parallelisierten Datenbanken und Webservern. Die Algorithmen sind datenstrukturspezifisch und synchronisieren den massiv parallelen Zugriff auf globale Datenstrukturen. Da sie sich nicht an das universelle Prinzip des gegenseitigen Ausschlusses halten, sind sie schwieriger zu entwickeln und auch die Korrektheitsbeweise sind deutlich komplexer.Ziel des beantragten Projekts ist die Entwicklung einer neuen, integrierten Methodik zur Spezifikation, inkrementellen Entwicklung (Verfeinerung), interaktiven Verifikation und automatisierten Analyse lock-freier Algorithmen. Das Vorhaben baut auf den Ergebnissen des früheren DFG Projekts INOPSYS auf, in dem eine sehr allgemeine Temporallogik und ein Kalkül zur interaktiven Verifikation paralleler Programme entwickelt wurde. Diese bilden den Rahmen für eine zu erarbeitende Methodik. Das Projekt baut außerdem auf einer Reihe von automatischen Techniken auf, die zur Verifikation spezieller Eigenschaften paralleler Algorithmen und lock-freier Algorithmen im Besonderen entwickelt wurden (Rely-Guarantee, Separation Logic, Shape Analysis etc.). Diese werden im Rahmen des Projekts in die interaktive Verifikation integriert.