Damian Sulewski:Parallelisierung eines Software Modellprüfers für nebenläufige C++ Programme
- nuovo livro ISBN: 9783836616041
Inhaltsangabe: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… mais…
Inhaltsangabe: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:Inhaltsverzeichnis: 1.Einführung1 1.1Vorwort1 1.2Annahmen2 1.3Struktur3 1.4Kontributionen3 2.Der Software Modellprüfer StEAM5 2.1Entstehung5 2.1.1Fehlertypen5 2.2Funktionsweise6 2.2.1Zustände und Abschnitte6 2.2.2Ablauf einer Prüfung7 2.2.3Ausgabe des Fehlerpfades9 2.3Suchalgorithmen10 2.3.1Ungerichtete Suche10 2.3.2Heuristiken11 2.3.3Gerichtete Suche12 2.4Speicherstruktur12 2.4.1Hashing12 Partielles Hashing13 2.4.2Kompression in StEAM13 2.5Vergleich mit anderen Software Modellprüfern13 2.5.1Verisoft14 2.5.2Bogor14 2.5.3Java Path Finder14 2.6Resümee15 3.Externalisierung17 3.1Motivation17 3.1.1Vorüberlegungen18 3.1.2Unterschiedliche Arten der Externalisierung18 3.2Speicherstruktur19 3.2.1Minizustand19 3.2.2Speicherung der Zustände im Hauptspeicher19 3.2.3Erweiterung der Collapse Kompression20 3.3Der Algorithmus21 3.3.1Komprimieren und Auslagern der Zustände22 3.3.2Dekomprimieren und Lesen der Zustände22 3.4Zugriff auf das sekundäre Medium22 3.4.1Single File Externalisierung23 3.4.2Hash File Externalisierung23 3.5Experimente24 3.6Resümee26 4.Virtualisierung29 4.1Speicherzugriff29 4.1.1Konvertieren der Adressen vor der Ausführung30 4.1.2Virtuelle Adressierung31 Angeforderte Speicherbereiche31 Globale Variablen und der Programmzähler32 Der Stack32 4.1.3Implementierung und Analyse33 Erkennen von unzulässigen Speicherzugriffen im MemoryPool33 4.1.4Analyse der Zugriffszeit34 4.1.5Experimente34 4.2Zugriff auf eine virtuelle Maschine35 4.2.1Zweck einer virtuellen Maschine35 4.2.2Identifikation der benötigten Methoden36 4.2.3Implementierung des Interfaces37 4.3Resümee38 5.Parallelisierung41 5.1Einbindung der Externalisierung42 5.1.1Effiziente Nutzung interner Festplatten42 5.2Kommunikation zwischen den Knoten43 5.2.1Verschicken von Zuständen43 5.2.2Zwei-Wege-Kommunikation44 5.2.3Duplikatseliminierung45 5.3Verteilungsfunktionen45 5.3.1Verteilung entsprechend einem Hashwert46 5.3.2Verteilung entsprechend einem partiellen Hashwert46 5.3.3Verteilung entsprechend der Tiefe46 5.3.4Verteilung entsprechend einem heuristischen Wert47 5.4Implementierung48 5.4.1Netzwerkkommunikation48 5.4.2Verteilung der Zustände48 5.4.3Der Algorithmus48 Minizustände zur Übermittlung von Status Nachrichten48 Empfangen und Expandieren der Zustände50 Zustände zur Expansion ermitteln50 5.5Experimente51 5.5.1Benutzte Hardware51 5.5.2Ergebnisse51 5.6Resümee54 6.Fazit55 ADie verwendeten Modelle57 A.1Speisenden Philosophen57 A.2N-Puzzle59 A.3Bakery Protokoll60 Literaturverzeichnis63Textprobe: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. Parallelisierung eines Software Modellprüfers für nebenläufige C++ Programme: Inhaltsangabe: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), Diplomica Verlag<
