Automatische Analyse nebenläufiger Pointerprogramme

• Antragsteller: Professor Dr. Thomas Noll
• Fachliche Zuordnung: Softwaretechnik und Programmiersprachen ; Theoretische Informatik
• Förderung: Förderung von 2015 bis 2020
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 276397324

Viele Softwarefehler sind auf die falsche Verwendung von Pointern,d.h. Verweisen auf Speicheradressen, zurückzuführen. Diese stellenein wesentliches Konzept moderner Programmiersprachen dar undwerden zur Implementierung dynamischer Datenstrukturen wie Listen,Bäumen usw. verwendet, welche im Computerspeicher in Form desso genannten Heaps verwaltet werden. Aufgrund derUnbeschränktheit der resultierenden Zustandsräume sindPointerfehler bereits in sequentieller Software schwer zu erkennen.Nebenläufigkeit (in der Form von Threads oder Prozessen) birgtverschiedene zusätzliche Herausforderungen, die durch gegenwärtigeVerifikationstechniken nur zum Teil abgedeckt werden. Aufbauend aufunserem graphbasierten Framework zur symbolischen Verifikation(sequentieller) Pointerprogramme lieferte das urprüngliche Projektwichtige Beiträge, welche durch die Entwicklung automatisierter undmodularer Techniken zur Analyse nebenläufiger Threads und durchdie Integration logik- und automatenbasierter Ansätze ermöglichtwurden. Insbesondere konnte die Mächtigkeit von Verfahren zurAnalyse relationaler Eigenschaften von Datenstrukturen (wie z.B.Balanciertheit) durch die Erweiterung von Graphgrammatiken um dasKonzept der Indizes signifikant gesteigert werden. Das Ziel desgeplanten Fortsetzungsprojekts besteht darin, den graphbasiertenAnsatz im Hinblick auf die Überprüfung von Inklusionsbeziehungenzwischen Heapdarstellungen, die Unterstützung weiterer Klassendynamischer Datenstrukturen und nebenläufiger Konstrukte vonProgrammiersprachen sowie die automatische Generierung vonTestfällen deutlich zu verbessern. Dazu werden wir die formalenZusammenhänge zwischen den graph- und automatenbasiertenAnsätzen herausarbeiten und das Konzept der indiziertenGraphgrammatiken weiterentwickeln. Darüber hinaus werden wir die"permission"-basierte Methode zur modularen Threadanalyseverfeinern, um genauere Informationen über Heapzugriffe zugewinnen und Synchronisationsmechanismen zu unterstützen,welche über das "fork-join"-Modell hinausgehen. Aus diesemForschungsprojekt werden neuartige Techniken, Algorithmen undTools zur symbolischen formalen Analyse relationaler Eigenschaftenvon dynamischen Datenstrukturen hervorgehen, die durchnebenläufige Pointerprogramme manipuliert werden. Ihre praktischeVerwendbarkeit soll anhand geeigneter Fallstudien wie verschiedenerArten (balancierter) Listen- und Baumstrukturen mit entsprechendenOperationen untersucht werden, wobei insbesondere Lock-freienebenläufige Datenstrukturen und parallele Sortierverfahrenberücksichtigt werden sollen.

• DFG-Verfahren: Sachbeihilfen
• Mitverantwortlich: Professor Dr. Joost-Pieter Katoen