Verifikation Asynchroner Programme 

Verifikation nebenläufiger Programme

Moderne Softwaresysteme werden immer komplexer. Zudem verlässt sich unsere Gesellschaft auf sie für immer wichtigere Aufgaben. Daher ist es sehr schwierig und zugleich äußerst wichtig, ein Verständnis dafür zu entwickeln, wie wir die Korrektheit einer bestimmten Software verifizieren können. Diesem Ziel widmet sich das Forschungsgebiet der Software-Verifikation.

Eine Quelle der Komplexität moderner Softwaresysteme ist die Nebenläufigkeit (engl. Concurrency): Es handelt sich dabei um die Tatsache, dass mehrere Code-Teile - aus Gründen der Einfachheit nennen wir diese Ausführungsstränge Threads - gleichzeitig ausgeführt werden können.

Das Verhalten solcher Systeme ist oft sehr schwer vorherzusagen:

Jeder einzelne Thread wird sequenziell ausgeführt, also so, wie dies die/der Programmierer*in im Code beschreibt. Aus der gleichzeitigen Code-Ausführung kann sich jedoch eine große Vielfalt an möglichen Abfolgen von Ereignissen ergeben.

Daher ist es schwierig, Programme zu schreiben, die sich in jeder möglichen Situation wie beabsichtigt verhalten. Dies macht Software-Verifikation unumgänglich. Wegen der enormen Menge von Verhaltensweisen stellt dies allerdings eine riesige Herausforderung dar.

Man denke beispielsweise an einen Webserver, der Tausende von Anfragen pro Sekunde beantworten muss. Jede einzelne Anfrage wird von einem Thread des Servers bearbeitet. Meistens greift hier jeder Thread auf eine Datenbank zu. Daher ist es leicht vorstellbar, dass das Betrachten aller erdenklichen Folgen von Datenbankanweisungen eine immense Aufgabe ist.

Leider ist nach einem bekannten Ergebnis der theoretischen Informatik (die Unentscheidbarkeit des Halteproblems, bewiesen von Alan Turing in 1936) eine vollautomatische Verifikation beliebiger Programme unmöglich: Wir können kein Programm P so schreiben, dass P uns immer sagt, ob ein gegebenes anderes Programm Q korrekt ist, wenn wir Q als Eingabe an P übergeben.

Ein wichtiger Forschungsansatz ist somit das Finden von Programmiersprachen, die zwar nicht so viel leisten wie allgemeine Sprachen, jedoch im Gegenzug eine automatische Verifikation erlauben. Eine solche Programmiersprache entspricht einer Programmklasse, die analysefähig ist.

Asynchrone Programme

Ein Beispiel für eine solche Programmklasse ist inspiriert vom Programmierparadigma der asynchronen Programmierung, welche eine eingeschränkte Form der Nebenläufigkeit bietet.

In einem asynchronen Programm kann jeweils nur ein einziger Thread gleichzeitig ausgeführt werden. Ein Thread kann jedoch in einen Task-Puffer Aufgaben posten, die dann für eine spätere Ausführung gesammelt werden. Sobald ein Thread abgeschlossen ist, wird eine neue Aufgabe aus dem Task-Puffer entnommen, wodurch dann der nächste Thread gestartet wird, und so weiter.  Dieses Paradigma wird häufig bei Low-Level-Systemsoftware und der Web-Programmierung sowie bei Benutzeranwendungen auf mobilen Plattformen verwendet.

In unserer Programmklasse gehen wir nun davon aus, dass jeder Thread rein rekursiv ist: Das bedeutet, dass alle Variablen nur endlich viele Werte annehmen können, wobei Funktionsaufrufe erlaubt sind.

Tatsächlich erlaubt diese Programmklasse - asynchrone Programme mit rein rekursiven Threads - eine automatische Verifikation:  Es gibt Algorithmen, die automatisch sogenannte "Safety-Eigenschaften" verifizieren. Solche Eigenschaften drücken zum Beispiel aus: Eine bestimmte Variable kann nie einen bestimmten Wert annehmen.

Um die folgenden Erläuterungen zu vereinfachen, meinen wir mit dem Begriff „Verifikation“ immer Safety-Eigenschaften.

Leider sind asynchrone Programme mit rein rekursiven Threads stark eingeschränkt:

In jedem Thread können wir zwar Funktionsaufrufe durchführen. Die Argumente können jedoch nur endlich viele Werte annehmen. Allerdings erwarten Programmierer*innen heute auch, Features funktionaler Programmiersprachen zu nutzen, wo man Funktionen als Argumente von Funktionen übergeben kann. Dies wird als Rekursion höherer Ordnung bezeichnet.

Asynchrone Programme höherer Ordnung und darüber hinaus

Es besteht somit die Notwendigkeit, asynchrone Programme höherer Ordnung zu verifizieren. Tatsächlich wäre es sogar wünschenswerter, wenn es für eine beliebige Klasse C von Thread-Programmen eine Prozedur für "Asynch(C)" gäbe, also die Klasse von asynchronen Programmen, in der jeder Thread zu C gehören kann. Deshalb wollten wir verstehen, wie stark man eine Klasse C von Thread-Programmen einschränken muss, um asynchrone Programme in Asynch(C) verifizieren zu können.

Das überraschende Ergebnis: Fast überhaupt nicht.

Lassen Sie uns das erläutern. Die Verifikation von Asynch(C)-Programmen ist eine viel schwierigere Aufgabe als die Verifikation von Programmen aus C: Programme in Asynch(C) sind nebenläufig und verfügen über einen Task-Puffer, zusätzlich zu der von C angebotenen Funktionalität. Daher würde man erwarten, dass wir C, bei einer Verifikation von Asynch(C), deutlich mehr einschränken müssen, als wenn wir nur Programme aus C verifizieren wollten.

Unter üblichen Annahmen zeigen wir jedoch: Falls Programme aus C verifiziert werden können, dann sogar die gesamte Klasse Asynch(C).

Wir haben somit eine überraschend einfache Charakterisierung, was im Bereich der Software-Verifikation selten ist. Zudem ist unser Algorithmus anwendbar auf asynchrone Programme höherer Ordnung und sogar weit darüber hinaus.

Zukünftige Arbeiten

Unser Ansatz zur Verifikation ist zwar überraschend flexibel, aber leider ineffizient. Daher wollen wir in unserer zukünftigen Arbeit untersuchen, wie wir asynchrone Programme höherer Ordnung effizienter verifizieren können.

Dies ist eine gemeinsame Arbeit mit R. Majumdar und R. S. Thinniyam am MPI-SWS.

Sie ist erschienen im Tagungsband der Konferenz TACAS 2021 und wurde von der European Association for Programming Languages and Systems (EAPLS) mit dem Best Paper Award ausgezeichnet.

Literaturhinweise