Trace-basierte dynamische Analyse von nebenläufigen Programmen

• Antragsteller: Professor Dr. Martin Sulzmann, Ph.D.; Professor Dr. Peter Thiemann
• Fachliche Zuordnung: Theoretische Informatik ; Softwaretechnik und Programmiersprachen
• Förderung: Förderung seit 2015
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 281466659

Wir betrachten Algorithmen zur dynamischen Vorhersage von Data-Races und Deadlocks auf der Grundlage von Programmtraces. Solche Algorithmen können nicht gleichzeitig effizient, korrekt und vollständig sein. Unser Ziel ist die Entwicklung verifizierter Algorithmen, die schnell genug sind um auf große Programme angewendet werden zu können und gleichzeitig einen guten Kompromiss bezüglich Korrektheit und Vollständigkeit liefern. Unsere Algorithmen sollen möglichst lineare Laufzeit haben und dabei sowohl wenige falsch positive als auch wenige falsch negative Befunde aufweisen. Besonderes Augenmerk legen wir auf Algorithmen, welche eine der folgenden Eigenschaften haben: Garantiert keine falsch positiven Befunde; garantiert keine falsch negativen Befunde; keine falsch positiven Befunde unter Einschränkungen wie z.B. die Anzahl der Programm-Threads oder die Einhaltung von Locking Protokollen. Die formale Spezifikation unserer Algorithmen basiert auf Charakterisierungen von falsch positiven/negativen Befunden und Bedingungen, unter denen sie vermieden werden können. Ein weiterer Schwerpunkt liegt auf Analyseaspekten, die bisher vernachlässigt wurden: Neue Kombinationen von Analysemethoden basierend auf Happens-before Beziehungen und Lockset Ansätzen; Kommunikationsmuster, die über einfache Lock-Protokolle hinausgehen (z. B. gepufferte Kommunikation); Programmierunterstützung durch detaillierte Diagnose sowie Heuristiken zur Programmreparatur; sowie der Umgang mit möglicherweise ungenau aufgezeichneten Programmtraces.

• DFG-Verfahren: Sachbeihilfen