Test and Verification of Compiler Back Ends with a Cost-Benefit Analysis

Test und Verifikation von Compiler-Backends mit einer Kosten-Nutzen-Analyse

  • Compilers are increasingly used for the development of safety-critical software applications. For these applications, it can lead to serious consequences if the compiler introduces a failure into the compiled program. Quality assurance techniques are required in particular for compiler back ends because they are known to be error-prone. The reason for this is that compiler back ends comprise complex optimizations and cannot be reused due to their dependence on the target processor. In this thesiCompilers are increasingly used for the development of safety-critical software applications. For these applications, it can lead to serious consequences if the compiler introduces a failure into the compiled program. Quality assurance techniques are required in particular for compiler back ends because they are known to be error-prone. The reason for this is that compiler back ends comprise complex optimizations and cannot be reused due to their dependence on the target processor. In this thesis, we present a formal verification as well as a testing approach for compiler back ends, which can be generated from a specification. With the presented verification approach we prove that the semantics of the compiled programs is preserved by the transformation that is defined in the back end specification. We developed a modular, machine-assisted verification approach within the theorem prover Isabelle/HOL. Our formalization enables us to decompose the overall correctness proof for a set of code generator rules into simpler proofs for individual rules, which are verified in isolation. We achieve this with the formalization of intermediate transformation results that are only implicitly present during compilation. In order to reduce the proof effort, we exploit the similarity that shows up in similar proofs and semi-automatize them by combining several proof steps into a single step. We capture in our formal model specification features that are required for the efficient development of industrial compilers. Our test approach allows for the automatic and systematic test of the generated back end. We exploit the fact that the back end specification defines a context free grammar. We derive from this grammar a test specification for combinatorial interaction testing(CIT). This enables us to apply a CIT test set generation algorithm in order to determine a test set that ensures rule combination coverage for a user-defined combination strength. Our test selection approach is a novel solution for the generation of test sets in grammar-based testing. We create the selected test cases by extending the compiler with a test generation module that is also derived from the back end specification. A generated test case is translated into an executable program and also into a source language program such that we can employ differential testing with an alternative compiler as automatic test evaluation method. In addition to our approaches, we also present their cost-benefit assessment. We defined assessment criteria in order to evaluate the approaches with regard to their employment for industrial compiler development projects. Our analysis identifies the benefits and relates them with the cost factors. The presented criteria provide guidance for the selection of the appropriate approach. Moreover, we present in this thesis two novel algorithms for CIT test set generation. Both algorithms are based on the conceptually new idea of the explicit representation of the test set. The experimental results with our algorithms exceed those of previously presented algorithms, which demonstrates the strength of this new concept.show moreshow less
  • Die Bedeutung der Software-Qualitätssicherung für Compiler hat in den letzten Jahren stark zugenommen. Übersetzt ein Compiler eine sicherheitskritische Software fehlerhaft, kann dies schwerwiegende Folgen haben. Insbesondere für Compiler-Backends werden effiziente Maßnahmen zur Überprüfung benötigt, da diese aufgrund der Abhängigkeit von der Zielarchitektur nicht wiederverwendbar sind und komplexe fehleranfällige Optimierungen enthalten. In dieser Arbeit präsentieren wir einen Verifikations- undDie Bedeutung der Software-Qualitätssicherung für Compiler hat in den letzten Jahren stark zugenommen. Übersetzt ein Compiler eine sicherheitskritische Software fehlerhaft, kann dies schwerwiegende Folgen haben. Insbesondere für Compiler-Backends werden effiziente Maßnahmen zur Überprüfung benötigt, da diese aufgrund der Abhängigkeit von der Zielarchitektur nicht wiederverwendbar sind und komplexe fehleranfällige Optimierungen enthalten. In dieser Arbeit präsentieren wir einen Verifikations- und einen Testansatz für die Qualitätssicherung von Compiler-Backends, die aus einer Spezifikation generiert werden können. Der von uns entwickelte Verifikationsansatz erbringt den formalen Beweis, dass die in der Spezifikation beschriebene Transformation aus der Compiler-internen Darstellung in den Maschinencode die Semantik der Programme erhält. Der von uns entwickelte Ansatz basiert auf einer Formalisierung im interaktiven Theorembeweiser Isabelle/HOL. Wir haben ein modulares Beweisverfahren entwickelt, mit dem die Korrektheit einer Menge von Spezifikationsregeln, mit Hilfe von Beweisen für die einzelnen Regeln bewiesen wird. Dies wird erreicht, indem die im Compiler nur implizit vorhandenen Transformationsergebnisse im formalen Modell explizit erfasst werden. Für die Beweisführung definieren wir Strategien, die Ähnlichkeiten in Beweisen ausnutzen und eine teilautomatisierte Beweisführung ermöglichen. Wir erfassen in unserem Ansatz Spezifikationsmöglichkeiten, die für die effiziente Entwicklung industrieller Compiler notwendig sind. Der von uns entwickelte Testansatz ermöglicht es, das generierte Backend systematisch und automatisiert zu testen. Um die Tests auszuwählen, extrahieren wir die in der Backendspezifikation vorhandene kontextfreie Grammatik. Aus dieser Grammatik leiten wir eine Testspezifikation für das kombinatorische Testen ab und können dann die Testfallmenge mithilfe eines Generierungsalgorithmus für kombinatorisches Testen berechnen. Unser Ansatz stellt eine neuartige Lösung für die Testauswahl beim grammatik-basierten Testen dar und garantiert, dass die Regelkombinationsmöglichkeiten systematisch getestet werden. Ein ausgewählter Testfall wird im Compiler mithilfe eines aus der Spezifikation automatisch abgeleiteten Moduls generiert und anschließend sowohl in Maschinencode als auch in die Quellsprache des Compilers übersetzt. Dieses Vorgehen ermöglicht es, die Testfälle automatisiert mithilfe eines alternativen Compilers als Testorakel zu bewerten. Wir stellen in dieser Arbeit eine Bewertung der Anwendbarkeit der beiden Qualitätssicherungsansätze für die entwicklungsbegleitende Absicherung von industriellen Compilern vor. Wir haben Bewertungskriterien definiert und die Ansätze anhand dieser Kriterien evaluiert. Mithilfe unserer Kriterien haben wir den Nutzen und die Kostenfaktoren der entwickelten Ansätze eindeutig identifiziert. Unsere Analyseergebnisse ermöglichen es, den für die Erfordernisse eines Projektes notwendigen Ansatz auszuwählen. Außerdem haben wir zwei Algorithmen für die kombinatorische Testfallgenerierung entwickelt. Beide Algorithmen basieren auf der konzeptuell neuen Idee der expliziten Repräsentation der vollständigen Testfallmenge. Die experimentellen Ergebnisse für diese Ansätze übertreffen die bekannter Algorithmen, was die Stärke dieses neuen Konzepts zeigt.show moreshow less

Download full text files

Export metadata

  • Export Bibtex
  • Export RIS

Additional Services

Share in Twitter Search Google Scholar
Metadaten
Author: Elke Salecker
URN:urn:nbn:de:kobv:83-opus-36852
Advisor:Prof. Dr. Sabine Glesner
Document Type:Doctoral Thesis
Language:English
Date of Publication (online):2012/09/26
Publishing Institution:Technische Universität Berlin
Granting Institution:Technische Universität Berlin, Fakultät IV - Elektrotechnik und Informatik
Date of final exam:2012/06/22
Release Date:2012/09/26
Tag:Compiler; Kombinatorisches Testen; Qualitätssicherung; Theorembeweisen
combinatorial interaction testing; compiler; quality assurance; theorem proving
Institutes:Institut für Softwaretechnik und Theoretische Informatik
Dewey Decimal Classification:004 Datenverarbeitung; Informatik
Licence (German):License LogoDeutsches Urheberrecht mit Print on Demand (u.a. für Dissertationen empfohlen)