| Popis: |
Entwickler profitieren heutzutage von einer Vielzahl an Optimierungen, welche moderne Compiler automatisch anwenden. Transformationen wie Methoden-Inlining, Constant Folding oder Escape Analysis spielen eine wichtige Rolle um die Laufzeitleistung zu verbessern. Gleichzeitig bringen derartige Optimierungen jedoch meist auch Nachteile mit sich. So ergeben sich für Ahead-of-Time (AOT) Compiler durch die angewandten Optimierungsalgorithmen sowie die Analyse des Programmcodes längere Build-Zeiten. Noch mehr befangen sind Just-in-Time (JIT) Compiler, da sie Programme zur Laufzeit compilieren, womit weitere Optimierungen diesen Prozess möglicherweise verzögern. GraalVM ist eine moderne Java Virtual Machine, spezialisiert auf derartige Optimierungen. Der Graal JIT Compiler analysiert Laufzeitinformation, welche von laufenden Programmen gesammelt und später zur Erzeugung von hochgradig optimiertem Maschinencode verwendet wird. Die dabei angewandten Optimierungen basieren zumeist auf etablierten Mustern, sowie bewährten Heuristiken, um Optimierungsziele in Programmen zu finden bzw. deren Konformität festzustellen. Die Integration von formale Methoden könnte dabei Abhilfe schaffen, neue Optimierungen festzustellen und zu beweisen - manuelles Vorgehen wird durch die Vielzahl an Optimierungsschritten zwischen dem Programm- und dem resultierenden Maschinencode erheblich erschwert. In dieser Arbeit beschreiben wir unseren Ansatz zur Integration einer Symbolic Execution Engine in den Graal Compiler, um damit automatisiert neue Optimierungsziele zu identifizieren. Symbolic Execution hilft uns dabei, aus der Zwischensprache des Compilers (Graal IR) logische Formeln zu generieren, welche die Programmsemantik beschreiben und es uns gleichzeitig ermöglichen, entsprechende Optimierungen zu prüfen und zu beweisen. In einem nächsten Schritt können so gefundene Muster als native Optimierungsphasen in den Compiler integriert werden. Auf diesem Ansatz basierend, entwickelten wir im Laufe unserer Arbeit eine Compilerphase für den Graal Compiler, welche mithilfe von Symbolic Execution verschiedenste Optimierungsziele erkennen kann. Benchmarks sowie vorhandene Graal-Test-Suites brachten dabei eine Reihe bisher unbekannter Optimierungen hervor, darunter Vereinfachungen arithmetischer bzw. Fließkommaoperationen, sowie Erkennung redundanter Vergleiche und aussagenlogischer Operationen. Darüber hinaus ergab die Arbeit an der Symbolic Execution Engine mehrere Bugs in modernen Theorembeweisern. Unsere abschließende Evaluierung der Arbeit und der gefundenen Optimierungsmuster konnte in Microbenchmarks Leistungssteigerungen von bis zu 15% zeigen. Modern compilers apply many different optimizations to programs without additional input from the developer. Method inlining, constant folding and escape analysis represent just some of the possibilities by which program code may be transformed to increase run time performance. Naturally, with each optimization there is also a trade-off: For ahead-of-time (AOT) compilers it implies longer build time, as more time is spent on analyzing the source code. Just-in-Time (JIT) compilers are even more affected, as they take longer until optimization is done and the compiled code is available. The GraalVM is a state-of-the-art Java Virtual Machine which specializes in such optimizations. The Graal JIT compiler actively gathers profiling information during program execution as to then use it for generating highly optimized machine code. While existing optimization phases are based on established patterns and heuristics to identify targets, formal methods may reveal further optimization potential via logical reasoning. The number of optimizations and the transformation which source code undergoes before being compiled, make it even harder for developers to manually identify promising optimization targets, let alone verify them. This thesis proposes an approach for integrating symbolic execution into the Graal compiler in order to find new optimization candidates automatically. By utilizing the intermediate representation of the Graal compiler, we can generate holistic formulas from methods to enable reasoning about individual expressions and statements. This process allows us to search for optimization patterns which may in turn be implemented as actual compiler phases. We showcase a custom optimization phase for the Graal compiler and multiple optimization techniques, which we evaluated on a variety of benchmarks as well as the Graal compiler test suite. Our findings include several bug reports for high-performance theorem provers, as well as multiple optimization patterns not yet recognized by the Graal compiler, including arithmetic operations, floating-point computations, and Boolean simplifications. An evaluation of identified optimizations showed performance improvements of up to 15% in microbenchmarks. submitted by Sebastian Kloibhofer, BSc Abweichender Titel laut Übersetzung der Verfasserin/des Verfassers Universität Linz, Masterarbeit, 2020 (VLID)5472240 |
