Resource Bound-Analyse von Lisp-Programmen

Abstract

Resource Bound Analysis ist ein Bereich der Programmanalyse, der sich mit der Bestimmung von Bounds (Grenzen) für die Menge an bestimmten Ressourcen, die beim Durchlauf eines Programms verbraucht werden, beschäftigt. Bounds sind Ausdrücke über die Eingabeparameter eines Programms, die für beliebige Kombinationen von Parametern korrekt sein sollten, was durch einfaches Testen nicht erreichbar ist. Die Analysetypen, die hier behandelt werden, sind statisch (d.h. es ist nicht notwendig, das Programm auszuführen, um einen Bound zu bestimmen) und vollständig automatisiert. Bounds für viele verschiedene Arten von Ressourcen sind von Interesse, darunter Laufzeit, Stack und Heap-Ausnutzung oder wie oft eine bestimmte Funktion aufgerufen wird. Resource Bound Analysis hat zahlreiche Anwendungsmöglichkeiten in der Entwicklung von Embedded- und Echtzeitsystemen, Komplexitätsanalyse von Algorithmus-Implementierungen, Security und weiteren, die wir detaillierter beschreiben. Viele neuere Ansätze und Implementierungen zielen auf imperative Programme ab. Im Gegensatz dazu konzentriert sich diese Arbeit auf funktionale Programme, wo Wiederholung (der wichtigste Aspekt in der Resource Bound Analysis) als rekursive Funktionsaufrufe statt als Schleifen implementiert ist. Da Ressourcenanalyse ein umfangreiches und komplexes Thema ist, beschränken wir unsere Analyse auf die Berechnung von Bounds für die Anzahl an Funktionsaufrufen und damit, wie oft jeder Teil des Programms ausgeführt wird. Wir legen allerdings dar, dass damit das Kernproblem gelöst ist und eine Erweiterung auf andere Ressourcentypen auf dieser Grundlage relativ einfach wäre. Wir präsentieren eine Boundanalyse für eine seiteneffektfreie Untermenge von Common Lisp mit Funktionen erster Ordnung. Die Analyse baut auf CoFloCo auf, einem existierenden Boundanalysesystem, das Bounds aus einem System von Cost Relations berechnet. Wir beschreiben eine Übersetzung von Lisp in Cost Relations, die die Berechnung korrekter Bounds für Lisp-Programme mit polynomieller Komplexität ermöglicht. Wir berichten über Experimente, die mit einem umfangreichen Benchmark durchgeführt wurden, das aus zusammen mit dem Theorembeweiser ACL2 verteilten Lisp-Programmen besteht. Insgesamt analysierten wir 19,491 Funktionen in 1,934 Dateien. Das Benchmark enthält Code für Modelle, die für Theorembeweise in industriellen Anwendungen wie etwa Hardware- und Mikrocodeverifikation verwendet wurden. Dasselbe Benchmark wurde außerdem bereits für die Evaluation des Terminationsbeweisers CCG verwendet, der in ACL2 enthalten ist. Wir untersuchen die erhaltenen Bounds und asymptotischen Komplexitätsergebnisse sowie die Laufzeit der Analyse als wichtigen Aspekt für praktische Anwendungen von Programmanalyse, um die Eignung unseres Ansatzes zu beurteilen und verbleibende (technische wie fundamentale) Probleme zu identifizieren.