Please use this identifier to cite or link to this item: http://dx.doi.org/10.14279/depositonce-3342
Main Title: Test and Verification of Compiler Back Ends with a Cost-Benefit Analysis
Translated Title: Test und Verifikation von Compiler-Backends mit einer Kosten-Nutzen-Analyse
Author(s): Salecker, Elke
Advisor(s): Glesner, Sabine
Granting Institution: Technische Universität Berlin, Fakultät IV - Elektrotechnik und Informatik
Type: Doctoral Thesis
Language: English
Language Code: en
Abstract: 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- 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.
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 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.
URI: urn:nbn:de:kobv:83-opus-36852
http://depositonce.tu-berlin.de/handle/11303/3639
http://dx.doi.org/10.14279/depositonce-3342
Exam Date: 22-Jun-2012
Issue Date: 26-Sep-2012
Date Available: 26-Sep-2012
DDC Class: 004 Datenverarbeitung; Informatik
Subject(s): Compiler
Kombinatorisches Testen
Qualitätssicherung
Theorembeweisen
Combinatorial interaction testing
Compiler
Quality assurance
Theorem proving
Usage rights: Terms of German Copyright Law
Appears in Collections:Technische Universität Berlin » Fakultäten & Zentralinstitute » Fakultät 4 Elektrotechnik und Informatik » Institut für Softwaretechnik und Theoretische Informatik » Publications

Files in This Item:
File Description SizeFormat 
Dokument_8.pdf1,35 MBAdobe PDFThumbnail
View/Open


Items in DepositOnce are protected by copyright, with all rights reserved, unless otherwise indicated.