Parallelisierung eines Software Modellprüfers für nebenläufige C++ Programme

Diplomarbeit von Damian Sulewski

Einleitung:

Immer mehr Bereiche in unserem Leben werden durch Technik bestimmt. Musste man vor einiger Zeit den Wecker noch jeden Abend neu aufziehen, wechselt man heute nur ab und zu die Batterien. Die Zeit kommt, Atom-Uhr genau, per Funk. Baute man im Mittelalter Burgen ca. 30 km voneinander entfernt (dies entspricht der Distanz, die ein Mensch am Tag zu Fuß zurücklegen konnte) können wir heute nahezu jeden Ort der Welt innerhalb von 24 Stunden erreichen.

Nicht nur das Vordringen moderner Technik in immer mehr Lebensbereiche, auch die Weiterentwicklung dieser Technik, ob zur Steigerung der Lebensqualität oder zur Erhöhung der Sicherheit, stellt eine Herausforderung an Prüfmechanismen dar. Klingelt der Wecker morgens aufgrund eines Programmfehlers nicht, so ist dies nicht tragisch. Entscheidet aber eine Software aufgrund eines Modellierungsfehlers bei einer Landung eines Flugzeugs nicht zu bremsen, kann dieses sogar Menschenleben kosten.

Eine bis heute gängige Prüfmethode ist das Testen (Gelperin:Testing; Hetzel:Testing). Hierbei werden nach einem vorher bestimmten Ablaufplan nahezu alle Eigenschaften des Modells geprüft, die Prüfungen ausgewertet und gegebenenfalls Fehler eliminiert. Diese Methode ist nicht nur sehr zeitaufwändig, sondern auch nicht unbedingt zuverlässig. Da die Tests von Menschen ausgewählt werden, können unwahrscheinliche, jedoch fatale Fehler übersehen werden. Hinzu kommt der riesige Zeit- und Arbeitsaufwand, der nötig ist, um umfangreiche Software-Projekte zu überprüfen. Natürlich muss der Aufwand in nahezu gleichem Umfang wiederholt werden, falls ein Fehler entdeckt und entfernt wurde.

Bei Software, an die besonders hohe Sicherheitsanforderungen gestellt werden (zum Beispiel Software die in lebenserhaltenden Geräten eingesetzt wird) ist eine andere Vorgehensweise notwendig. Es werden Fehlerbedingungen in einer so genannten Metasprache definiert und die Software in diese Sprache übersetzt (Holzmann:Spin; ksu:bogor). Das so entstandene Modell kann nun von einem Modellprüfer (Clarke:ModelChecking) gelesen und bezüglich der Fehlerbedingungen verarbeitet werden. Verletzt die Software eine der Bedingungen so wird sie als Fehlerhaft eingestuft. Da die Übersetzung meist von Hand vorgenommen wird, entstehen zwei potentielle Quellen für falsche Testergebnisse. Erstens kann ein Fehler der während einer Prüfung diagnostiziert wurde, beim Übersetzten hinzugefügt worden sein. Zweitens ist es möglich, dass ein Fehler nicht erkannt wird, da dieser bei der Übersetzung unwissentlich korrigiert wurde, in der Software allerdings weiterhin existiert. Des Weiteren kann eine Modellprüfung nur Fehler diagnostizieren die in der Metasprache formuliert werden können.

Software Modellprüfer (Godefroid:Verisoft; Visser:JPF) sind hingegen in der Lage, Quelltexte zu prüfen. Sie haben Ihre Wurzeln in der abstrakten Interpretaion (Cousot:AbsInt) und der Datenflussanalyse (Steffen:DFA) Die vom Entwickler erstellte Software wird gelesen in einer kontrollierten Umgebung ausgeführt und auf Fehler untersucht. Fehlerbedingungen können sowohl in den Quelltext, als auch in den Prüfer eingebunden werden. StEAM (Mehler:Dissertation), ein am Lehrstuhl für Programmiersysteme der Universität Dortmund entwickelter Software Modellprüfer, der innerhalb dieser Diplomarbeit erweitert wurde, verarbeitet die Programmiersprache C++ (Stroustrup:Cpp). Bei dieser Sprache handelt es sich um eine höhere Programmiersprache, die sowohl eine maschinennahe, als auch eine Programmierung auf hohem Abstraktionsniveau ermöglicht. Das Programm wird in einer virtuellen Maschine (Visser:mcp) ausgeführt, die von StEAM kontrolliert wird.

Automatische Verifikationsmethoden kämpfen mit einem Problem: Der Anzahl der möglichen Programmzustände. Ein Programmzustand ist ein Abbild des Programms zu einem bestimmten Zeitpunkt. Beim Testen werden zumeist so viele unterschiedliche Programmzustände erzeugt, dass die Ressourcen (Zeit oder Systemspeicher) nicht ausreichen, um komplexe Programme zu überprüfen. Bei der Software Modellprüfung gibt es mehrere Ansätze, um diesem Phänomen zu begegnen , z.B. (Jard:Memory; Lafuente:PartialOrder; Holzmann:Bitstate). Ein möglicher Ansatz ist die in dieser Arbeit beschriebene Externalisierung und Parallelisierung. Dabei wird der Zustandsraum auf mehrere Rechner verteilt, um so Zugang zu größeren Ressourcen zu erhalten. Da die einzelnen Knoten unterschiedliche, unabhängige Programmzustände untersuchen, erwarten wir so eine schnellere Antwort. Kombiniert mit der Vereinigung von Hauptspeicher können auch komplizierte Software Modelle untersucht werden. Diese Methode klingt verlockend, da sie auf den ersten Blick leicht skaliert. Falls die gegebene Anzahl an Rechenknoten nicht ausreicht, fügt man weitere hinzu. Dabei muss man aber eines beachten. Wendet der Algorithmus zu viel Zeit für die Kommunikation zwischen Rechenknoten auf, so geht der Zeitvorteil, der durch die Benutzung mehrerer Rechner erlangt wurde, verloren.

Ziel dieser Diplomarbeit war demnach den Software Modellprüfer StEAM zu parallelisieren und mehrere Rechner, die über ein Netzwerk verbunden sind, zur Überprüfung des Modells zu verwenden. Dabei sollte der zu entwickelnde Algorithmus, über geeignete Verteilungsfunktionen, nicht zu viele Ressourcen für die Kommunikation verwenden, aber auch sicherstellen, dass Zustände nicht mehrfach expandiert werden. Der Modellprüfer muss natürlich weiterhin in der Lage sein, einen Fehlerzustand zu finden und den Fehlerpfad korrekt auszugeben. Des Weiteren sollte analysiert werden, ob eine striktere Trennung, zwischen StEAM und der virtuellen Maschine, weitere Möglichkeiten zur Modellprüfung eröffnet.

Inhaltsverzeichnis:

1.	Einführung	1
1.1	Vorwort	1
1.2	Annahmen	2
1.3	Struktur	3
1.4	Kontributionen	3
2.	Der Software Modellprüfer StEAM	5
2.1	Entstehung	5
2.1.1	Fehlertypen	5
2.2	Funktionsweise	6
2.2.1	Zustände und Abschnitte	6
2.2.2	Ablauf einer Prüfung	7
2.2.3	Ausgabe des Fehlerpfades	9
2.3	Suchalgorithmen	10
2.3.1	Ungerichtete Suche	10
2.3.2	Heuristiken	11
2.3.3	Gerichtete Suche	12
2.4	Speicherstruktur	12
2.4.1	Hashing	12
	Partielles Hashing	13
2.4.2	Kompression in StEAM	13
2.5	Vergleich mit anderen Software Modellprüfern	13
2.5.1	Verisoft	14
2.5.2	Bogor	14
2.5.3	Java Path Finder	14
2.6	Resümee	15
3.	Externalisierung	17
3.1	Motivation	17
3.1.1	Vorüberlegungen	18
3.1.2	Unterschiedliche Arten der Externalisierung	18
3.2	Speicherstruktur	19
3.2.1	Minizustand	19
3.2.2	Speicherung der Zustände im Hauptspeicher	19
3.2.3	Erweiterung der Collapse Kompression	20
3.3	Der Algorithmus	21
3.3.1	Komprimieren und Auslagern der Zustände	22
3.3.2	Dekomprimieren und Lesen der Zustände	22
3.4	Zugriff auf das sekundäre Medium	22
3.4.1	Single File Externalisierung	23
3.4.2	Hash File Externalisierung	23
3.5	Experimente	24
3.6	Resümee	26
4.	Virtualisierung	29
4.1	Speicherzugriff	29
4.1.1	Konvertieren der Adressen vor der Ausführung	30
4.1.2	Virtuelle Adressierung	31
	Angeforderte Speicherbereiche	31
	Globale Variablen und der Programmzähler	32
	Der Stack	32
4.1.3	Implementierung und Analyse	33
	Erkennen von unzulässigen Speicherzugriffen im MemoryPool	33
4.1.4	Analyse der Zugriffszeit	34
4.1.5	Experimente	34
4.2	Zugriff auf eine virtuelle Maschine	35
4.2.1	Zweck einer virtuellen Maschine	35
4.2.2	Identifikation der benötigten Methoden	36
4.2.3	Implementierung des Interfaces	37
4.3	Resümee	38
5.	Parallelisierung	41
5.1	Einbindung der Externalisierung	42
5.1.1	Effiziente Nutzung interner Festplatten	42
5.2	Kommunikation zwischen den Knoten	43
5.2.1	Verschicken von Zuständen	43
5.2.2	Zwei-Wege-Kommunikation	44
5.2.3	Duplikatseliminierung	45
5.3	Verteilungsfunktionen	45
5.3.1	Verteilung entsprechend einem Hashwert	46
5.3.2	Verteilung entsprechend einem partiellen Hashwert	46
5.3.3	Verteilung entsprechend der Tiefe	46
5.3.4	Verteilung entsprechend einem heuristischen Wert	47
5.4	Implementierung	48
5.4.1	Netzwerkkommunikation	48
5.4.2	Verteilung der Zustände	48
5.4.3	Der Algorithmus	48
	Minizustände zur Übermittlung von Status Nachrichten	48
	Empfangen und Expandieren der Zustände	50
	Zustände zur Expansion ermitteln	50
5.5	Experimente	51
5.5.1	Benutzte Hardware	51
5.5.2	Ergebnisse	51
5.6	Resümee	54
6.	Fazit	55
A	Die verwendeten Modelle	57
A.1	Speisenden Philosophen	57
A.2	N-Puzzle	59
A.3	Bakery Protokoll	60
	Literaturverzeichnis	63

Textprobe:

Kapitel 3.2, Speicherstruktur:

Um sowohl dem Problem der Zustandsgröße, als auch der "Zustandsexplosion" zu begegnen, wurde die Idee von Minizuständen entwickelt.

Minizustand:

Die Minizustände (engl. ministates) verbleiben im Speicher und stellen ein Skelett des Zustandsraums dar. Da die Größe eines Minizustands konstant ist, kann vor einer Prüfung errechnet werden, wie viele Minizustände erzeugt werden, bis der Hauptspeicher aufgebraucht ist. Die konstante Größe der Minizustände ist auch der größte Vorteil dieser Idee. Während die Anzahl der Zustände, die im Speicher gehalten werden können, von deren Größe abhängt, ist es mit Hilfe der Minizustände möglich, sogar Zustände zu untersuchen, die nahezu den gesamten Hauptspeicher eines Rechners einnehmen.

Des Weiteren dient ein Minizustand lediglich als Referenz auf einen Zustand. Dieser kann sich im Hauptspeicher oder auf einem weiteren Medium befinden, der Zugriff über einen Minizustand ermöglicht, ihn jederzeit zu lokalisieren.

Da die einzige Voraussetzung, die ein Minizustand erfüllen soll, eine konstante Größe ist, wurden noch weitere Informationen aufgenommen, die eine Prüfung erleichtern oder beschleunigen.

Speicherung der Zustände im Hauptspeicher:

Wird ein neuer Zustand erzeugt, so wird dieser nicht sofort auf die Festplatte geschrieben, sondern verbleibt im Speicher. Der Speicherbereich, in dem Zustände aufbewahrt werden, wird Zustand-Cache genannt. Zusätzlich enthält der zugehörige Minizustand eine Referenz auf den Zustand. So kann direkt, über den Minizustand, auf einen Zustand zugegriffen werden. Der Zustand-Cache ist eine einfach verkettete Liste, die als Least-Recently-Used (LRU) Struktur gehandhabt wird. Wird ein Zustand der sich im Cache befindet, gelesen - sei es um ihn zu expandieren, oder ihn auf Duplikate zu prüfen - so wird seine Referenz in der Liste auf Position eins verschoben. Auf diese Weise wird sichergestellt, dass Zustände, die nicht gebraucht werden, ans Ende der Liste wandern. Ein Cache wurde so konzipiert, dass die Reihenfolge, in der Zustände ausgelagert werden, frei wählbar ist. So ist es möglich, über die Verwendung unterschiedlicher Techniken (z.B. Last-In-First-Out (LIFO), First-In-First-Out (FIFO), Least-Frequently-Used (LFU), Flush-When-Full (FWF), etc.) den Cache an den Suchalgorithmus anzupassen.

Die Anzahl der Zustände, die der Zustand-Cache aufnehmen kann, ist, statisch (beim Start durch einen User) oder dynamisch (durch Expandierung) begrenzt. Wird die maximale Größe erreicht, so werden die Zustände, die sich am Ende der Liste befinden, also die die am längsten nicht benötigt wurden, gelöscht. Natürlich erfolgt vor dem Löschen eine Speicherung. Geschrieben wird aber nicht nur der zu löschende Zustand, sondern alle Zustände, die noch nicht gespeichert wurden. Die Tatsache, ob ein Zustand bereits auf die Festplatte abgelegt wurde, kann direkt aus dem jeweiligen Minizustand gelesen werden. Ist die fid, also die Nummer der Datei in der sich ein Zustand befindet, positiv, so wurde dieser bereits gespeichert. Wird ein Zustand gelöscht, so wird die Referenz state, im entsprechenden Minizustand, auf NULL gesetzt. Abbildung 3.2 zeigt eine schematische Darstellung der Funktionsweise.

Erweiterung der Collapse Kompression:

Wie bereits beschrieben, unterstützt StEAM Kompression. Es werden lediglich die Abschnitte der Vorgänger auf Gleichheit geprüft, so konnten identische Abschnitte mehrfach im Speicher existieren. Um den Speichernutzung vor einer Externalisierung zu optimieren, wurde die vollständige Funktionalität der ”Collapse Compression” implementiert (Edeletal:ExternalProgramMC).

StEAM beinhaltet nun mehrere Cache Strukturen, die jeweils einen Abschnitt eines Zustandes aufnehmen können. Wird ein Zustand dem Zustand-Cache hinzugefügt, so wird er vorher in einzelne Abschnitte zerlegt. Jeder Abschnitt wird in den entsprechenden Cache eingefügt, der eine Zahl id zurückliefert, die den Abschnitt im Cache eindeutig identifiziert. Die id wird im Zustand gespeichert und die direkte Referenz auf den Abschnitt gelöscht. Nachdem dies für alle Abschnitte des Zustandes durchgeführt wurde, besteht der Zustand nun aus einem Ganzzahlvektor.

Dieser Vorgang wird für jedes wiederholt, so erhält man einen Ganzzahlvektor:

Die Größe ist nicht konstant da sich

P

während der Ausführung ändern kann. Sie wird dann in den Zustand-Cache eingefügt.

Bevor ein Abschnitt in den Cache eingefügt wird, muss eine id berechnet werden. Als id wird der, für den entsprechenden Abschnitt berechnete partielle Hashwert k(sec) mit sec verwendet. Tritt eine Kollision auf, so wird der errechnete Hashwert inkrementiert und als id verwendet. So ist sichergestellt, dass jeder Abschnitt eines Caches eine id erhält. Aufgrund von Kollisionen kann k(sec) nicht als eindeutige Identifikationsnummer verwendet werden. Intern werden die Sektionen in einem AVL-Baum gespeichert, so dauert ein Einfügen höchstens O(logn), wobei n die Anzahl der Elemente im Cache bezeichnet.

Zusätzlich zu dem AVL-Baum verwaltet jeder Cache eine einfach verkettete Liste, die der im Zustand-Cache entspricht. Ein Hinzufügen läuft nach dem selben LRU-Schema, wie ein Hinzufügen eines Zustandes zum Zustand-Cache. So ist auch hier sichergestellt das Abschnitte die seltener gebraucht werden, in der Liste hinten aufbewahrt werden.

Um den internen Speicherverbrauch zu reduzieren, wurde die Größe dieser Caches beschränkt. Jeder Cache hat eine maximale Größe. Wird diese überschritten, werden Elemente, die sich am Ende der Liste befinden, externalisiert. Der AVL-Knoten verbleibt dabei im Speicher um die Information aufzunehmen, wo sich die Daten des Abschnitts auf der Festplatte befinden. Wird der Abschnitt wieder benötigt, kann er leicht rekonstruiert werden.