Tree Constraint Solver (TCS) - Löser linearer Baumungleichungen für superlineare Verbrauchsschranken an Java-Programmen

• Antragstellerin: Dr. Sabine Bauer
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung von 2019 bis 2021
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 432878302

Dieses Projekt hat das Ziel, beweisbar korrekte obere Schranken an den Ressourcenverbrauch unannotierter Javaprogramme zu ermitteln. Derartige automatische Ressourcenanalysen werden immer bekannter und sind auch in der Wirtschaft stark nachgefragt. Momentan liegt der Schwerpunkt der analysierbaren Programme bei funktionalen oder klassischen imperativen Programmen mit Arrays als wichtigster Datenstruktur. Wir bauen auf der etablierten Theorie der typenbasierten amortisierten Analyse auf, die in der funktionalen Welt mit großem Erfolg eingesetzt wurde. Die Objektorientierung bietet allerdings neue Herausforderungen: a) die Datenstrukturen sind implizit durch Klassenhierarchien definiert und nicht explizit wie bei funktionalen Datentyp-Deklarationen, b) das imperative Update kann zu komplizierten Alias-Datenstrukturen führen, c) es sind allgemeinere Datenstrukturen wie doppelt verkettete Listen oder auch beliebige Graphen möglich.In Vorarbeiten wurde die Erarbeitung einer Lösungsstrategie für diese Fragestellungen begonnen, die eine Reduktion der Frage nach dem Ressourcenverbrauch auf die Erfüllbarkeit von neuartigen Ungleichungssystemen mit unendlich vielen numerischen Variablen verwendet (englisch ”linear tree constraints (LTC)”). Der dort entwickelte heuristische Löser für die Ungleichungen ist jedoch auf bestimmte Spezialfälle beschränkt. In sehr neuen Arbeiten wurde gezeigt, dass die Gesamtheit dieser Ungleichungen entscheidbar ist. Wir vermuten, dass sie darüber hinaus auch in der Praxis effizient handhabbar sind, und möchten dies in diesem Projekt genau erforschen. Wir werden eine Lösungsmethode mit optimaler Laufzeitkomplexität für die Ungleichungen entwickeln und implementieren, die es ermöglicht, konkrete Schranken an den Speicherplatzverbrauch von objekt-orientierten Programmen zu berechnen. Dafür ist die Entscheidbarkeit alleine nicht ausreichend, vielmehr müssen wir minimale Lösungen der Ungleichungen als geschlossene Formeln ausdrücken. Ferner müssen wir die exakte Komplexität des Entscheidungsproblems ermitteln, und anschließend einen Lösungsalgorithmus finden, der in diese Komplexitätsklasse fällt. Die Tatsache, dass die Entscheidbarkeit selbst bereits bewiesen ist, stellt aber einen guten Startpunkt dar und macht ein Gelingen des gesamten Vorhabens wahrscheinlich. Wir werden die erzielten Resultate nutzen, um ein Analyseframework für imperative objekt-orientierte Programme zu designen und es mit einer Prototyp-Implementierung an einer Vielzahl von Beispielprogrammen in Java-Syntax testen.

• DFG-Verfahren: Sachbeihilfen