ZIDline
Systematisches Testen eines Constraint-Systems
Ulrich Neumerkel, Institut für Computersprachen

Die Studenten-PCs in den Internet-Räumen des ZID sind mittels CONDOR zu einem Campus-Grid (WINZIG) zusammengefasst, dessen beachtliche Rechenleistung zu Nacht- und Wochenendzeiten für Scientific Grid-Computing genutzt werden kann. Dieser Grid wird vom Institut für Computersprachen zum Testen der CLP(FD)-Implementierung von SWI-Prolog eingesetzt.

Im letzten Jahr wurde das Constraint-System CLP(FD) von SWI-Prolog [0] – einem frei verfügbaren System – von Markus Triska innerhalb seiner Masterarbeit [1] entwickelt und seitdem kontinuierlich verbessert. Dabei wurde versucht, die Beschränkungen bestehender Systeme aufzuheben [2], um Constraints auch in der Lehre [3] und in neuen Anwendungsbereichen wie Verifikation, Programmanalyse [4] und Diagnose einsetzen zu können. Gerade in diesen Bereichen kommt der Korrektheit des Systems eine zentrale Bedeutung zu. Traditionell waren Constraint-Systeme eher auf größtmögliche Effizienz für einen sehr eng ausgelegten Anwendungsbereich optimiert. Neue Verwendungen führen in bestehenden Systemen oft zu falschen Ergebnissen oder Nichttermination.

Um die Entwicklung von CLP(FD) für SWI-Prolog bestmöglich zu unterstützen, habe ich systematische Tests entwickelt, die laufend an das System angepasst werden. Anfänglich wurden die Tests auf den Institutsrechnern durchgeführt, bis schließlich der von WINZIG [5] verwaltete Condor-Grid des ZID zum Einsatz kam. Seit mehr als einem halben Jahr und über mehr als 90 CPU-Jahre hinweg wird nun die CLP(FD)-Implementierung von SWI-Prolog getestet. Dabei konnten viele Fehler gefunden werden – einige sogar in zentralen Teilen des Systems und selbst im darunter liegenden SWI-Prolog.

Die Adaptierung und der effektive Betrieb der Testläufe erforderten beträchtliche Umstellungen, die ich im Folgenden nach einer kurzen Beschreibung der Tests erörtern möchte.

Testkriterien

Beim systematischen Testen [6] wird nach der Verletzung von algebraischen Eigenschaften – wie Monotonie oder Kommutativität – gesucht. Es wird nicht gegen eine vollständige Spezifikation getestet, die ja ihrerseits wieder fehlerbehaftet sein könnte, sondern man beschränkt sich auf „unmittelbar ersichtliche“ Eigenschaften. So sollten etwa die folgenden Anfragen aufgrund der Kommutativität der Konjunktion zum gleichen Ergebnis führen.

  ?- X in 0..2, 0/X #= 0,
     X = 1.

  ?- X = 1,
     X in 0..2, 0/X #= 0.

In diesem Fall scheiterte aber die erste Anfrage, während die zweite eine Lösung fand. Allein aufgrund dieses Unterschieds kann man bereits sagen, dass eine der beiden Anfragen fehlerhaft ist – möglicherweise sogar beide. Es ist also nicht erforderlich, die Eigenheiten der involvierten Konstrukte – etwa der Division – zu kennen. Lediglich die Vertauschung der Ziele ist hier von Relevanz. Die weitere Diagnose, welche Anfrage nun wirklich richtig ist – in diesem Falle letztere – wird einer manuellen Bearbeitung überlassen, schließlich treten derartige Fehler sehr selten auf und ziehen ohnehin entsprechende Programmiertätigkeiten nach sich.

Ein systematisches Testen muss nun mögliche Kandidaten in geeigneter Weise aufzählen. Der Suchraum ist hier dermaßen groß, dass weitere Einschränkungen vonnöten sind. So wird nur der Wertebereich -3...3 betrachtet. Auch werden gezielt Fälle mit gemeinsamen Variablen betrachtet, da diese erfahrungsgemäß eine nie versiegende Fehlerquelle sind. Es hat sich als günstig erwiesen, nur einen Teil der Formel zu generieren, und dann durch Erweiterungen die eigentlichen Kandidaten zu erzeugen. Der Formelteil wird fortlaufend durchnummeriert. So lassen sich Testläufe einfach durch Angabe der Nummer reproduzieren.

Bei den ersten Testläufen am Institut wurde die Menge der Formeln auf eine fixe Zahl von vorhandenen Threads aufgeteilt. Mittels der Formelnummer konnte jeder Prozess für sich ohne weiteren Kommunikationsaufwand seinen Teil abarbeiten. Leider führte diese Aufteilung zu einer besonders schlechten Auslastung. Manche Prozesse waren rasch fertig, während anderen Prozessen die gesamte Rechenarbeit zufiel. Dies rührt daher, dass die Zeit zur Überprüfung der Kandidaten einer Formel sehr stark variiert – zwischen Sekundenbruchteilen und einer Woche. Auch durch die recht unzuverlässige Stromversorgung am Institut wurde die Rechenleistung geschmälert.

Condor

Der Condor-Grid unter WINZIG macht die Nutzung noch etwas komplizierter.

  • Die meisten Rechner sind nur in den Nachtstunden verfügbar.
  • Durch andere Nutzer mit höherer Priorität werden Prozesse selbst in dieser Zeit unterbrochen.
  • Rechner fallen im Betrieb unangemeldet aus.
  • Rechner liefern falsche Resultate – wahrscheinlich bedingt durch Speicherfehler.
  • Transiente Fehler – wie das Fehlen des Filesystems.
  • Hoher Verwaltungsaufwand pro Prozess. Jeder Prozess sollte i.d.R. zumindest 5 Minuten benötigen.
  • Bei geringerer Rechenzeit übersteigt bald der Verwaltungsaufwand den Nutzen.
  • Es sollten insgesamt nicht mehr als 5000 Prozesse gleichzeitig von Condor verwaltet werden. Mehr Prozesse dürften die Verteilungseinheit überfordern.
  • Der Speicherbedarf eines Prozesses ist sehr stark limitiert.
  • Die Mechanismen für Checkpoints sind zu aufwändig und unzuverlässig.

Diesen Nachteilen stehen die folgenden Vorteile gegenüber

  • Derzeit bis zu 300 parallele Threads.
  • Zuverlässige Prozessverwaltung und Reproduzierbarkeit über Jahre hinweg.

Die folgenden Anpassungen waren erforderlich, um die Testläufe effizient durchführen zu können.

Verminderung des Speicherverbrauchs

Auf den Condor-Rechnern stehen Prozessen ausschließlich der Hauptspeicher zur Verfügung. Es gibt keinen Swap-Space. Prozesse, die zu viel Speicher benötigen, brechen mit einer entsprechenden Fehlermeldung ab. Es gibt hier praktisch keine Möglichkeit, diese Limitation zu umgehen. Die vorhandenen Programme müssen also notfalls inhaltlich umgeschrieben werden, um unter diesen eingeschränkten Bedingungen zu funktionieren.

Erhöhung der Granularität

Es werden derzeit 100 Formeln in einen Prozess zusammengefasst. Dadurch reduziert sich der Verwaltungsaufwand für sehr kurze Prozesse auf ein Hundertstel.

Checkpoints

Da der bestehende Checkpoint-Mechanismus sich als weder zuverlässig noch effizient herausstellte, wurde ein eigener Mechanismus entwickelt. Nach jeder Formel und an bis zu 100000 Stellen innerhalb einer Formel wird ein Checkpoint in das NFS-Filesystem geschrieben. Dabei werden ausschließlich die Formelnummer sowie zwei ähnlich geartete Nummern für Zwischenzustände angegeben. Die Gesamtgröße dieser Datei beträgt nur wenige Bytes. Um sicherzustellen, dass nicht zu oft geschrieben wird, werden Zwischenzustände höchstens alle 2 Minuten geschrieben. Die anderen Zwischenzustände werden nicht gesichert und sind ggf. als roll-back zu verbuchen.

Prozessverwaltung

Die Prozessverwaltung ist in Condor sehr mächtig. Allerdings ist zu beachten, dass Prozesse, die einmal aus der Verwaltung ausscheiden, nicht mehr zurückgeholt werden können. Aus diesem Grund empfiehlt es sich, nur Prozesse mit erfolgreichem ExitCode aus der Verwaltung zu entlassen. Alle anderen Prozesse, also jene, die mit einem Fehlercode abbrechen oder zu einem Bus-Error oder ähnlichem geführt haben, sollen im Wartezustand verharren. Nach eingehender Untersuchung oder Korrektur können diese wieder gestartet oder gelöscht werden. Mit folgender Zeile im Submission-File wird dies bewerkstelligt.

on_exit_hold = ExitBySignal || ( ExitCode != 0 )

Im Condor-Manual wird empfohlen, bei fehlerhaftem Abbruch eines Prozesses diesen sogleich erneut zu starten. Dies scheint nicht wirklich sinnvoll, weil dadurch fehlerhafte Prozesse das gesamte System lahmlegen könnten.

Schluss

Im Nachhinein erscheinen die für Condor erforderlichen Adaptierungen gar nicht so exotisch, wie sie anfangs aussahen. Auch in anderen Kontexten ist es sinnvoll, einen Checkpoint-Mechanismus zu verwenden und sich über den Verwaltungsaufwand von Prozessen Gedanken zu machen. Mittlerweile verwenden alle Testläufe den anfangs für Condor entwickelten Mechanismus, selbst wenn sie nicht unter Condor laufen.

Ich möchte mich bei Herrn Philipp Kolmann für die viele Rechenzeit und perfekte Wartung des WINZIG-Systems bedanken.

Referenzen

[0] http://www.swi-prolog.org/

[1] M. Triska, Solution Methods for the Social Golfer Problem. Masterarbeit, TU Wien, 2008.

[2] M. Triska, U. Neumerkel, J. Wielemaker. A Generalized Finite Domain Constraint Solver for SWI-Prolog. WLP 2008.

[3] U. Neumerkel, M. Triska, J. Wielemaker. Declarative Language Extensions for Prolog Courses. FDPE 2008.

[4] A. Prantl, J. Knoop, M. Schordan, M. Triska. Constraint solving for high-level WCET analysis. WLPE 2008.

[5] Ph. Kolmann. University Campus Grid Computing, Diplomarbeit, TU Wien, 2005.

[6] M. Triska, U. Neumerkel, J. Wielemaker. Better Termination for Prolog with Constraints. WLPE 2008.