Automatisches Überprüfen nebenläufiger Computerprogramme

Ein Computerprogramm ist eine Abfolge von Anweisungen, die bestimmte Eingabeargumente annimmt und ein Ergebnis berechnet. Unter der Annahme, dass wir eine Möglichkeit haben, zu bestimmen, ob ein gegebenes Eingabe-Ausgabe-Paar korrekt ist, können wir die Korrektheit eines Computerprogramms überprüfen, indem wir die Korrektheit der berechneten Ausgabe für jede mögliche Programmeingabe nachweisen. Bei diesem Prüfungsansatz gibt es jedoch zwei grundlegende Probleme.

Erstens kann es sein, dass das Programm bei einer bestimmten Eingabe zu keinem Ende gelangt. Aufgrund der Unentscheidbarkeit des Halteproblems [1] ist es unmöglich, das herauszufinden, ohne das Programm bis zum Ende auszuführen.

Zweites Problem: Die meisten Programme sind reaktiv. Sie nehmen nicht einfach eine statische Eingabe entgegen und berechnen ein Ergebnis, sondern interagieren mit dem Benutzer – über den Bildschirm, die Tastatur, die Maus – und/oder der Umgebung, zum Beispiel durch das Lesen von Sensordaten und das Ausführen von Aktionen.

In der Praxis lassen sich diese Probleme jedoch leicht beheben. Um erstens zu vermeiden, dass ein Programm nicht terminiert, können wir es für ein bestimmtes Zeitbudget, zum Beispiel fünf Sekunden, ausführen und es als fehlerhaft betrachten, wenn es nicht innerhalb dieses Zeitbudgets terminiert. Zweitens können reaktive Programme als Funktionen betrachtet werden, deren Eingaben die Abfolge früherer Interaktionen sind und deren Ausgabe der nächste Effekt eines Programms ist. Dies ähnelt einem Schachspiel, bei dem das Brett vollständig durch die Menge der früheren Züge bestimmt wird.

Nebenläufigkeit als Herausforderung

Es gibt jedoch ein viel schwierigeres Problem, das hinter der nächsten Ecke lauert: Nebenläufigkeit. Moderne Programme enthalten mehrere Threads von Anweisungen, die von verschiedenen Prozessoren gleichzeitig ausgeführt werden können. Ihre Ausgaben sind somit nicht mehr vollständig durch ihre Eingaben bestimmt – sie können von der relativen Ausführungsgeschwindigkeit der Prozessoren und von den Verzögerungen bei der gegenseitigen Kommunikation abhängen. Diese wiederum können von externen Faktoren abhängen, zum Beispiel davon, welche anderen Programme ebenfalls ausgeführt werden.

Zwar können prinzipiell alle diese Faktoren als Programmeingaben betrachtet werden, aber die Zahl der Eingaben nimmt astronomische Ausmaße an. Was können wir also tun?

Modellprüfung

Wir können eine „Modellprüfung“ (Model Checking) [2] durchführen, indem wir alle möglichen Reihenfolgen untersuchen, in denen die Programm-Threads ausgeführt werden können. Dabei können wir Optimierungen anwenden, um zu vermeiden, dass unterschiedliche Reihenfolgen untersucht werden, die zum gleichen Programmergebnis führen.

So können wir beispielsweise nebenläufige Anweisungen, die auf unterschiedliche Speicherorte zugreifen, immer in einer bestimmten Reihenfolge anordnen [3]. Außerdem können wir symmetrische Muster in den Programmen ausnutzen: Wenn mehrere Komponenten versuchen, dieselbe Aufgabe zu erfüllen, spielt es keine Rolle, welche von ihnen zuerst ausgeführt wird. Dank dieser und anderer Optimierungen lassen sich kleine, aber komplizierte nebenläufige Programme umfassend verifizieren [4].

Um größere Programme zu überprüfen, müssen wir jedoch den Fokus ändern. Anstatt die Korrektheit eines Programms zu beweisen, sollten wir versuchen, seine Fehlerfreiheit zu beweisen. Außerdem können wir ein Maß für die Komplexität eines Programmfehlers in Form einer Zahl definieren – zum Beispiel wie oft muss die Programmausführung unterbrochen werden, bis der Fehler auftritt. Wir können dann Ansätze zur „beschränkten Modellprüfung“ (Bounded Model Checking) entwickeln, die eine Fehlerfreiheit bis zu einer bestimmten Grenze feststellen und so aussagekräftige partielle Korrektheitsgarantien für nebenläufige Programme liefern [5].

Literaturhinweise