Effiziente Analyseverfahren für die Performability-Bewertung verteilter Systeme
Zusammenfassung der Projektergebnisse
Die in diesem Bericht präsentierten Forschungsergebnisse stehen im Zusammenhang mit der modellbasierten Leistungsbewertung auf Basis von Markov-Modellen. Heute ist es gängige Praxis, Markov-Modelle nicht mehr direkt zu spezifizieren, sondern dafür höhersprachliche Formalismen wie stochastische Petrinetze oder stochastische Prozessalgebren zu verwenden. Es existieren eine Reihe von Werkzeugen, die aus den höhersprachlichen Formalismen Markov-Modelle generieren können. Je detaillierter die Modelle werden, desto größer werden die entstehenden Markov-Ketten, man spricht von "Zustandsraumexplosion". Die Generierung der Modelle ist heute technisch gelöst: Nahezu beliebig große Zustandsräume von Markov-Modellen lassen sich in Sekundenschnelle aus der Modellspezifikation generieren. Dazu erstellt man das Gesamtmodell aus Teilmodellen, die ihrerseits wieder aus Teilmodellen aufgebaut sein können. Durch Synchronisationen sind normalerweise alle Komponenten von anderen Komponenten abhängig. Mit Hilfe von kompakten Datenstrukturen können die Modelle direkt aus der Spezifikation generiert und im Rechner gespeichert werden (z.B. durch Kronecker-Matrizen oder Multi-Terminale binäre Entscheidungsdiagramme (MTBDDs)). Während für Kronecker-Matrizen effiziente Algorithmen zur Bestimmung der stationären Zustandswahrscheinlichkeiten der Markov-Kette (insbesondere auch ein Multilevel-Algorithmus nach Horton und Leutenegger) existieren, war vor Beginn dieses Projektes noch kein MTBDD Algorithmus, der die spezielle Struktur der Modelle nutzen kann, bekannt. Die in diesem Projekt erarbeiteten Ergebnisse schließen diese Lücke. Es wurde ein praktikabler Ansatz für das Verfahren nach Horton und Leutenegger entwickelt, der sich komplett auf MTBDDs realisieren lässt und als Löser-Komponente prototypisch in das Werkzeug PRISM der Universität Oxford integriert wurde. Im Gegensatz zum Kronecker-basierten Multilevel Algorithmus, der für Aggregationen immer die Teilmodell-Grenzen (pro Teilmodell wird ein Teil der Gesamt-Matrix generiert) respektieren muss, kann der MTBDD-basierte Algorithmus nahezu beliebige Aggregationen durchführen, die nicht an Teilmodell-Grenzen gebunden sind. Während für hinreichend große Modelle Teilmodell-basierte Aggregation sehr gute Ergebnisse liefert, ist es für Modelle mit relativ wenig MTBDD Variablen sinnvoll, nicht Teilmodell-weise zu aggregieren (z.B. Tandem-Modell des PRISM Frameworks). Im Rahmen der Forschungsarbeit wurde ein neuer Offset-Labelling Algorithmus entwickelt, öer sowohl für die aggregierten als auch für das nicht-aggregierte Gleichungssystem die Offsets berechnet. Offsets ermöglichen eine kompakte Abbildung von der lückenhaften Menge der Zustands-Deskriptoren auf fortlaufende natürliche Zahlen. Die Forderung nach kompakter Speicherung der aggregierten Gleichungssysteme führte zu einer Charakterisierung von MTBDD- Knoten innerhalb der aggregierten MTBDD Variablen. Die aggregierten Werte reduzierbarer Knoten müssen nicht in jeder Iteration neu berechnet werden, sondern sie können einmal im Voraus berechnet und dann wieder verwendet werden. Der Speicheraufwand wird dadurch geringer, da jeder aggregierte Zahlenwert nur einmal im Speicher angelegt wird. Durch die Isomorphieregel für MTBDDs kann es vorkommen, dass ein Knoten sowohl als reduzibel, als auch als irreduzibel klassifiziert wird. Dieses Phänomen wurde analog zu den von Parker beobachteten Offset-Clashes als "Aggregation-Clash" bezeichnet. Um modernen Mehrkern-Prozessoren Rechnung zu tragen, wurde auch eine parallel ausführbare Version des Algorithmus erstellt. Während sich Vektoroperationen relativ leicht parallelisieren lassen, sind Matrix-Vektor Operationen (für Aggregation und Glättungsschritte) schwieriger zu handhaben. Die Datenstruktur für die Matrizen wurde entsprechend geändert, damit sie, verbunden mit einer heuristischen Lastverteilung, für Mehrprozessorbetrieb geeignet ist. Die im Rahmen dieses Projektes erstellten Datenstrukturen und Algorithmen ergänzen die Standard-Lösungsalgorithmen wie Gauss-Seidel, Jacobi und Power-Methode. Abhängig von der Struktur der Matrix ist der Multilevel-Algorithmus in der single-Thread Version um mehr als Faktor zwei schneller. Noch nicht vollständig erforscht ist, welche Aggregationsstrategien zur schnellsten Lösung führen. Eine Heuristik für Kronecker-basierte Multilevel-Verfahren ist es, entlang der Submodell-Grenzen zu aggregieren. Im MTBDD-Kontext gilt diese Regel nicht immer, wie durch ein Gegenbeispiel belegt wurde. Strenge Konvergenz-Aussagen für das verwendete Multilevel-Verfahren sind bisher nur in Spezialfällen bekannt. Sie eröffnen ein mehrdimensionales Analogon zu Julia-Mengen. Generelle Aussagen hierfür sind noch nicht bekannt.
Projektbezogene Publikationen (Auswahl)
- A symbolic multilevel method with sparse submatrix representation for memory-speed tradeoff. In 14. GI/ITG Conf. Measurement, Modelling and Evaluation of Comp., and Communic. Systems (MMB08), pages 191-205. VDE Verlag, 2008
J. Schuster and M. Siegle
- An Efficient Symbolic Elimination Algorithm for the Stochastic Process Algebra tool CASPA. In SOFSEM 2009: Theory and Practice of Computer Science, pages 485-496, Spindleruv Mlyn, Czech Republic, 2009. Springer, LNCS 5404
J. Bachmann, M. Riedl, J. Schuster, and M. Siegle
- Speeding up the symbolic multilevel algorithm. In M. Benzi and T. Dayar, editors, Procceedings of the Sixth International Workshop on the Numerical Solution of Markov Chains (NSMC 2010), pages 79-82, September 2010
J. Schuster and M. Siegle
- Symbolic calculation of k-shortest paths and related measures with the stochastic process algebra tool CASPA. In Proc. of the First Workshop on DYnamic Aspects in DEpendability Models for Fault-Tolerant Systems, pages 13-18, 2010
M. Günther, J. Schuster, and M. Siegle
- Path-based calculation of MTTFF, MTTFR, and asymptotic unavailability with the stochastic process algebra tool CASPA. In Proceedings of the Institution of Mechanical Engineers, Part 0: Journal of Risk and Reliability, September 2011
J. Schuster and M. Siegle
- Towards faster numerical solution of Continuous Time Markov Chains stored by symbolic data structures. PhD thesis, Universität der Bundeswehr München, 2011
J. Schuster
