Servicenavigation

Detailseite

Zurück

Projekt Druckansicht

Optimale Interprozeduale Analyse von Programmen mit dynamischer Thread-Erzeugung

Fachliche Zuordnung Softwaretechnik und Programmiersprachen
Förderung Förderung von 2007 bis 2017
Projektkennung Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 52609764
 
Erstellungsjahr 2017

Zusammenfassung der Projektergebnisse

Ein zentrales Thema des Projekts waren optimale Analysen für Programme mit rekursiven Prozeduren und dynamischer Threaderzeugung. Als Modellformalismus für derartige Programme verwendeten wir sogenannte dynamische Pushdown-Netzwerke (DPNs) und abstrahierten damit von unendlichen Datenbereichen und gemeinsam verwendeten Variablen. Aufbauend auf eigenen Vorarbeiten und Resultaten von Kahlon et al. konnten zunächst optimale Erreichbarkeitsanalysen für DPNs mit wohlgeschachtelt verwendeten Locks entwickelt werden, ein überraschendes und von uns ursprünglich nicht erwartetes Ergebnis, da andere Synchronisations- oder Kommunikationskonzepte zu unentscheidbaren Erreichbarkeitsproblemen führen. Wurden zunächst nur nicht re-entrante Locks und vergleichsweise einfache Erreichbarkeitsprobleme betrachtet, konnten die Verfahren später auch auf re-entrante Locks und Monitore sowie allgemeinere Analysefragestellungen erweitert werden. Auch gewisse Formen von join-Kommandos konnten optimal mitbehandelt werden, was wir ebenfalls urspünglich nicht erwartet hatten. Darüber hinaus haben wir die Entscheidbarkeit grundlegender Analyseprobleme von DPNs mit contextual locking gezeigt, einer von Chadha et al. vorgeschlagenen Lock-Disziplin, die über wohlgeschachtelte Verwendung hinausgeht, und die Komplexität dieser Probleme genauer charakterisiert. Ferner haben wir ein Verfahren entwickelt, das die Stärke der DPN-basierten Analysen für die präzisere Berechnung von Invarianten in parallelen Programmen mit gemeinsamen Variablen (shared state) nutzbar macht. Einige Varianten der DPN-basierten Analyseverfahren wurde implementiert, mithilfe des Wala-Frameworks an die Analyse von Java-Programmen angebunden und in einem experimentellen Analysator für data races verwendet. Ein weiteres wichtiges Thema innerhalb des Projekts war die Frage, inwiefern es möglich ist, exakte Analysen linearer Ungleichungen zu finden. Hier ermöglichte die neue Technik der Strategieiteration einen Durchbruch. Zumindest für muster-basierte Analysen ermöglichen die neuen Verfahren, die exakte kleinste Lösung der zugehörigen Gleichungssysteme auszurechnen. Die Idee der Strategieiteration wurde schließlich zu einer parametrischen Strategieiteration verallgemeinert. Im ganzzahligen Fall kann nun eine Aufteilung des Parameterraums in konvexe Bereiche berechnet werden, innerhalb derer für jedes Template die optimalen Schranken mit Hilfe desselben linearen Ausdrucks beschrieben werden kann. Bei dem Versuch, eine geeignete Infrastruktur zur Einbindung komplexer Analysen in ein Werkzeug zur statischen Analyse zu entwickeln, fiel unser Augenmerk generell auf Fixpunktalgorithmen zur bedarfsgetriebenen Analyse von Programmen. Unsere Untersuchungen zeigten, dass das bisherige Schema einer sukzessiven Iteration in eine Richtung, möglicherweise gefolgt von einer Iteration in die Gegenrichtung aufgegeben werden kann zugunsten einer Iteration, die lokal entscheidet, ob der gegenwärtige Wert vergröbert oder verfeinert werden soll. Als Testumgebung für die neuen Verfahren diente das System Goblint, mit dem nebenläufige C-Programme analysiert werden können. Die neuen Fixpunktalgorithmen ermöglichen, komplexere abstrakte Bereiche bei der Analyse zu verwenden und so die Genauigkeit zu erhöhen. Als besonders ergiebig erwies sich die Untersuchung nebenläufiger C-Programme unter Autosar/Osek. Für diese wurden Analysen für Dataraces sowie der Transaktionalität von Funktionen entwickelt. Wir bemühten uns auch um die Popularisierung unserer Ideen. In einer Veröffentlichung im Spektrum der Informatik werden verschiedene Ansätze zur Programmanalyse vorgestellt und auf ihre jeweiligen Vorzüge hin verglichen.

Projektbezogene Publikationen (Auswahl)

 
 

Zusatzinformationen

© 2024 DFG Kontakt / Impressum / Datenschutz

Textvergrößerung und Kontrastanpassung