Zusammenfassung:
Moderne Prozessoren haben meist mehrere Kerne. Die Rechenleistung eines Systems mit einem solchen Multi-Core Prozessor ist der eines Ein-Prozessor-Systems vor allem deshalb überlegen, weil mehrere Anwendungen parallel ausgeführt werden können. Eine einzelne Anwendung profitiert zunächst nur indirekt von mehreren Rechenkernen, da sie in der Regel nur einen Kern benutzt. Ausnahmen hiervon sind Programme, die mehrere Threads beinhalten, was aber gerade bei leistungskritischen Anwendungen meist nicht der Fall ist, da man bisher durch die nötige Synchronisation der Threads wertvolle Rechenzeit verschenkte. Bei einer Mehrprozessor-Architektur mit gemeinsamem Hauptspeicher kann nun eine Optimierung solcher Anwendungen durch Aufteilung des Programmflusses in mehrere nebenläufige Ausführungsstränge einen nicht unerheblichen Leistungszuwachs bedeuten. Diese Diplomarbeit dokumentiert eine solche Optimierung für den expliziten Model Checker CMC. Hierzu werden, anders als in anderen Ansätzen beim Model Checking mit Multi-Core Prozessoren, den Kernen verschiedene Teilaufgaben zugewiesen. Mithilfe des Komponentenframeworks von CMC wurde zunächst ein einfacher Model Checker implementiert, auf dessen Basis dann die multithread-fähigen Komponenten entwickelt und später in die aktuelle Implementierung von CMC integriert wurden.
Download:
thesis_final.pdf