Vergleich von seL4 und L4Re unter Leistungsge­sichtspunkten

Diese Arbeit beschäftigt sich mit den Mikrokernel-basierten Betriebssystemen L4Re und seL4. Die Leistung der Systeme bezüglich IPC-Latenzen, Speicher- und Dateioperationen wird untersucht. Für die IPC-Messungen wurden vorhandene Benchmarkprogramme verwendet. Die für L4Re bereitgestellten Programme für Speicher- und Dateioperationen wurden angepasst und nach Möglichkeit auf seL4 und Linux implementiert.
Durch wiederholte Messungen können die Ergebnisse statistisch ausgewertet werden. Dadurch ist die Angabe von Mittelwerten und Standardabweichungen möglich. Basierend auf diesen Zahlenwerten werden die Systeme verglichen und mögliche Ursachen für die Unterschiede werden angegeben.

(Verteidigung Bachelorarbeit)