Realistische Compiler

Einleitung

Ob es uns gefällt oder nicht: Softwaresysteme haben unser Leben erobert und sind nicht mehr wegzudenken. Unsere Industrie – egal, ob im Fertigungs-, Transport- oder Finanzsektor – ist zunehmend von Software abhängig geworden.

Gleichzeitig sind Computerprogramme mathematische Objekte, für die wir Theoreme aufstellen und beweisen können. Ein äußerst nützliches Theorem für ein Programm ist beispielsweise das „Sicherheits“-Theorem, das besagt, dass die Ausführung des Programms nicht zum Ausfall einer Maschine (oder eines Smartphones oder eines Autos!) führt. Ein noch viel nützlicheres Theorem – wenn auch ein viel schwieriger nachweisbares – besagt, dass das Programm tatsächlich das leistet, was es „vorgibt“ zu leisten. Aber wie lässt sich ein solches Theorem formalisieren und seine Richtigkeit zuverlässig nachweisen?

Genau damit beschäftigt sich die Softwareverifizierung. Sie bietet eine strikte Methodik, die formal spezifiziert, was Programme leisten sollen, und formal nachweist, dass die vorgegebenen Spezifikationen eingehalten werden. Anfänglich wurden formale Korrektheitsbeweise für Programme manuell durchgeführt, weshalb es als zu mühsam galt, sie für realistische Softwaresysteme durchzuführen. Jüngste Fortschritte in der interaktiven Theorem-Beweis-Technologie haben uns allerdings dem Traum von einer voll verifizierten Software wesentlich näher gebracht.

Ein Projekt in diesem Bereich, das für erhebliche Aufmerksamkeit gesorgt hat, ist das CompCert-Projekt unter der Leitung von Xavier Leroy am französischen Forschungsinstitut für Informatik und Automatik (INRIA). Leroy hatte sich vorgenommen, einen realistischen, vollständig verifizierten Compiler für einen Dialekt der Programmiersprache C [1] zu entwickeln. Um diese beeindruckende und bedeutende Leistung nachvollziehen zu können, muss man zunächst die zentrale Bedeutung von Compilern in unseren heutigen komplexen Softwaresystemen verstehen.

Verifiziertes Kompilieren

Die Softwarerevolution wurde durch zwei wesentliche Faktoren eingeläutet: (i) die kontinuierlichen Verbesserungen in der Computerhardware und (ii) die Entwicklung von höheren Programmiersprachen, etwa C/C++, Java und Python, mit denen man bei angemessenem Zeitaufwand robuste, umfangreiche Programme schreiben kann. Da die höheren Programmiersprachen ein hohes Maß an Abstraktion ermöglichen, können sich die Programmierer auf die von ihnen zu implementierenden Algorithmen konzentrieren, ohne sich Gedanken darüber machen zu müssen, wie diese Algorithmen auf Maschinenebene exakt in Bits und Registern abgebildet werden. Ohne höhere Programmiersprachen müssten die Programmierer alles direkt in einem Low-Level-Assembler-Code schreiben, der sich nur schwer anpassen und pflegen, geschweige denn korrekt programmieren lässt. Damit aber höhere Programmiersprachen auch einsetzbar sind, braucht man optimierende Compiler, die höhere Quellprogramme in für die Hardware verständliche effiziente Zielprogramme in Assemblersprache übersetzen.

Selbst sehr gut getestete Compiler enthalten viele Bugs: Eine Gruppe an der University of Utah [2] berichtete kürzlich von der Entdeckung von 325 Fehlern in Compilern wie llvm und gcc, den wichtigsten C/C++ Compilern, die von Apple bzw. Linux verwendet werden. Dies hat zu einer sehr misstrauischen Haltung der sicherheitskritischen Softwareindustrie gegenüber Compilern geführt. Sie vermeiden jetzt Features in den Programmiersprachen, die nach ihrer Einschätzung fehlkompiliert werden könnten, und überprüfen oft manuell, ob der kompilierte Assemblercode mit dem Quellprogramm übereinstimmt.

Was aber wäre, wenn man den Argwohn hinsichtlich der Fehlerfreiheit von Compilern dadurch zerstreuen und die manuelle Überprüfung ihrer Leistung dadurch umgehen könnte, dass man die Korrektheit der Compiler selbst beweist? Genau dieses Problem nahmen vor einigen Jahren Xavier Leroy und seine Kollegen am INRIA in Paris in Angriff und entwickelten einen neuen Compiler für die Programmiersprache C unter der Bezeichnung CompCert, dessen formelle Richtigkeit sie nachweisen konnten. Der Nachweis selbst ist relativ lang (rund 50.000 Zeilen), weil er die subtile Korrektheit einiger wichtiger Compiler-Optimierungen nachweisen muss, kann aber maschinell mit dem interaktiven Beweis-Assistenten Coq [3] kontrolliert werden.

Mit dem CompCert-Compiler wurde ein entscheidender Meilenstein in der Softwareverifizierung erreicht, beweist er doch die Machbarkeit von verifizierten Compilern, die sowohl im Sinne der durch sie kompilierten Programmiersprachen als auch der durch sie implementierten Optimierungen realistisch sind. Zwei wichtige Aspekte der realistischen Kompilierung werden jedoch vom CompCert nicht berücksichtigt. Deren Untersuchung haben wir uns am MPI für Softwaresysteme in unserem aktuellen Projekt zur Aufgabe gemacht.

Kompositionalität

Reale höhere Programmiersprachen sind oft sehr umfassend. Zwecks effektiver Handhabung solcher Programme zerlegt man sie normalerweise in viele kleinere Module, die nur über sorgfältig vorgegebene Schnittstellen im losen Zusammenhang stehen.

Ein entscheidender Vorteil dieser modularen Dekomposition besteht darin, dass jedes Modul in einem Programm gegenüber „lokalen“ Änderungen in anderen Teilen des Programms abgeschirmt ist. Nehmen wir beispielsweise den Kernel des Betriebssystems Linux. Wenn ein Modul, das einen Gerätetreiber implementiert, aktualisiert wird und sich die Aktualisierung nicht auf die Schnittstelle des Moduls auswirkt, müsste man nicht das gesamte Kernel rekompilieren, was mehrere Stunden in Anspruch nehmen würde, sondern lediglich den Gerätetreiber selbst. Ein weiterer praktischer Vorteil der modularen Dekomposition besteht darin, dass umfassende Programme aus mehreren unterschiedlichen Software-Bibliotheken, die nicht unbedingt alle in derselben höheren Programmiersprache geschrieben oder mit demselben Compiler kompiliert wurden, miteinander verbunden werden könnten.

Der CompCert-Compiler ist ein Compiler, der das ganze Programm optimiert. Er garantiert die Korrektheit der Kompilierung nur für Programme, die als ganzes Programm in der C-Programmiersprache geschrieben und mit CompCert kompiliert wurden. Idealerweise wünschte man sich jedoch einen Ansatz der kompositionalen verifizierten Kompilierung, bei dem die verschiedenen Programmmodule in unterschiedlichen Programmiersprachen geschrieben sein und mit verschiedenen verifizierten Compilern kompiliert werden können.

Die Unterstützung einer kompositionalen verifizierten Kompilierung erweist sich als sehr schwierig. Das hängt wesentlich damit zusammen, dass wir es mit zwei sich quasi entgegenstehenden Dimensionen der Kompositionalität zu tun haben, die wir als horizontal und vertikal (siehe Abb. 1) bezeichnen. Wie durch die roten Verbindungslinien angezeigt, bezieht sich die horizontale Kompositionalität auf die Fähigkeit, die Verifizierung verschiedener Compiler zu verknüpfen. Aber jeder Compiler an sich verursacht wiederum mehrere „Durchgänge“, die das Quellprogramm schrittweise in das Zielprogramm transformieren. Wie durch die grünen Verbindungslinien angezeigt, bezieht sich die vertikale Kompositionalität auf die wesentliche Fähigkeit, die Korrektheit eines einzelnen Compilers durch die transitive Zusammensetzung der Korrektheitsbeweise seiner konstituierenden Durchgänge zu verifizieren.

Sowohl die horizontale als auch die vertikale Kompositionalität zu erreichen, stellt eine große Herausforderung dar. Bestehende simulationsgestützte Techniken, wie sie CompCert verwendet, unterstützen die vertikale, nicht aber die horizontale Kompositionalität. Andere Methoden, die auf sogenannten logischen Relationstechniken basieren, unterstützen die horizontale, nicht aber die vertikale Kompositionalität [4, 5].

In einem anlässlich des diesjährigen POPL-Symposiums (Flaggschiff-Veranstaltung im Bereich Programmiersprachen) veröffentlichten Papier schlugen wir jedoch eine neue bahnbrechende Technik – Relationstransitionssysteme – vor, die die wichtigsten Aspekte von Simulationen und logischen Relationen vereint und deshalb sowohl die horizontale als auch die vertikale Kompositionalität unterstützen kann [6]. Es ist noch ein weiter Weg, bis die Effektivität der Relationstransitionssysteme in der Praxis demonstriert werden kann. Unsere bisherigen Ergebnisse sind jedoch vielversprechend.

Nebenläufigkeitsmodelle und Relaxed Memory-Modelle

Fortschritte in der Verarbeitungsleistung von Rechnern sind vor allem durch das Aufkommen von Multicore-Architekturen möglich geworden, die den gleichzeitigen Lauf mehrerer Programme oder mehrerer Threads in einem einzigen Programm zulassen. Damit solche Hardware effektiver eingesetzt werden kann, werden reale High-Level-Programme oft als nebenläufige Programme geschrieben, damit verschiedene Teile des Programms parallel in verschiedenen Threads laufen können.

Allerdings verkompliziert das Prinzip der Nebenläufigkeit die Verifizierung, weil man gezwungenermaßen berücksichtigen muss, wie sich die über die nebenläufig ausgeführten Threads gesteuerten Abläufe gegenseitig stören könnten. Zudem können die zahlreichen Threads eines nebenläufigen Programms möglicherweise aufgrund der systemnahen Hardwareoptimierungen und der Kommunikationslatenz zwischen den verschiedenen Kernen des Multicore-Chips keinen konsistenten Speicherabzug erkennen. Ihre Beobachtungen entsprechen eher einem Relaxed Memory-Modell, wie dem x86-TSO-Modell, das von den Mainstream-Prozessoren Intel und AMD (Abb. 2) implementiert wurde. Wann immer in diesem Modell ein Thread in ein Segment eines gemeinsam genutzten Speichers schreibt, erkennt es den aktualisierten Wert direkt (durch seine nächste Anweisung), werden aber die Threads, die in den anderen Kernen laufen, erst zu einem späteren Zeitpunkt über die Aktualisierung informiert.

Folglich können viele der traditionellen Compileroptimierungen, die für sequentielle Programme entwickelt wurden (d. h. Programme mit nur einem Thread), einschließlich einiger der in CompCert implementierten Optimierungen, durch Nebenläufigkeit invalidiert werden. Liest beispielsweise ein sequentielles Programm eine globale Variable mehrmals in einer Reihe, kann es so optimiert werden, dass es die globale Variable nur einmal liest und das Ergebnis für schnellere nachfolgende Zugriffe in einem lokalen Register abspeichert. In einem nebenläufigen Programm ist diese Optimierung jedoch inkorrekt, wenn die globale Variable simultan durch einen anderen Thread aktualisiert wird. Um diese Optimierung korrekt durchzuführen, muss der Compiler also in der Lage sein zu beweisen, dass die globale Variable nicht simultan von einem anderen Thread aktualisiert wird.

Leider erfüllt CompCert diese Anforderung nicht und kompiliert nebenläufige Programme deshalb möglicherweise falsch. Deshalb ist CompCert nur als korrekter Compiler für sequentielle Programme verifiziert. Im Hinblick auf dieses Problem haben wir den CompCert-Compiler und seinen Korrektheitsbeweis auf ein Nebenläufigkeitssetting hin angepasst, sodass im Ergebnis der erste verifizierte optimierende Compiler für nebenläufige Programme entstanden ist. Diese Arbeit ist Bestandteil des CompCertTSO-Projektes und wurde anlässlich des POPL-Symposiums 2011 veröffentlicht [7].