Aufzeichnungsbasierte Analyse von Sperren in Betriebssystemen

Abstract

Moderne Mehrkernbetriebssysteme bieten eine Vielzahl an Synchronisationsmechanismen. Sie dienen der Realisierung von feingranularem Sperren, um dem Betriebssystem wie auch den darauf laufenden Anwendungen zu erlauben, die Leistung von modernen Mehrkernprozessoren auszunutzen. Hierbei werden ganze Subsysteme, einzelne Datenstrukturen oder lediglich Teile einer Datenstruktur mit einer oder mehr Sperren abgesichert. Je vielfältiger die Mechanismen und je feingranularer das Sperren wird, desto fehleranfälliger kann ein Betriebssystem werden. Daher ist es immanent wichtig zu verstehen, wie die vorgenannten Synchronisationsmechanismen in einem Mehrkernbetriebssystem eingesetzt werden, um Synchronisationsfehler zu vermeiden. Existierende Forschungsarbeiten in diesem Bereich befassen sich mit dem Auffinden von spezifischen Synchronisationsproblemen, wie z. B. der Detektion von Wettlaufsituationen um Speicherzugriffe. Sie detektieren Synchronisationsfehler allerdings nur im Nachhinein. Sie leiten aber keinerlei Sperren-Regeln ab, die Aussagen über das korrekte Absichern von Zugriffen machen könnten. So würden im Vorhinein Fehler vermieden. Genau diese Lücke versucht die vorliegende Arbeit zu schließen. Daher befasst sie sich mit den Fragen, ob man a) mit der aufzeichnungsbasierten Analyse Erkenntnisse über das Synchronisationsverhalten in Mehrkehrbetriebssystemen erlangen kann, und, wie man b) mit diesen Erkenntnissen die Softwarequalität moderner Mehrkernbetriebssysteme verbessern kann. Daraus ergeben sich folgende Forschungsbeiträge dieser Arbeit: Zunächst wird in dieser Arbeit der Entwurf des LockDoc-Ansatzes erläutert. Dieser umfasst das Aufzeichnen von Speicherzugriffen und Sperren-Operationen in einem Betriebssystemkern, während eine Arbeitslast ausgeführt wird. Daraus werden Zusammenhänge zwischen Zugriffen auf Datenstrukturen und Sperren-Operationen hergestellt. Dies lässt sich auf dreierlei Wegen nutzen: 1) Das Überprüfen der existierenden Sperren-Dokumentation, ob der Programmcode sich noch an die dokumentierten Regeln hält. 2) Das Ableiten von neuen Sperren-Regeln für verschiedene Datentypen. Aus diesen Daten lässt sich in einem weiteren Schritt eine neue Sperren-Dokumentation generieren. 3) Das Detektieren von Zugriffen, die nicht den abgeleiteten Regeln folgen. Die sogenannten Gegenbeispiele zeigen potentielle Synchronisationsfehler inkl. der Aufrufhierarchie sowie den tatsächlich gehaltenen Sperren an. In dieser Arbeit wird der Ansatz im Rahmen von Fallstudien auf die Betriebssystemkerne von Linux und FreeBSD angewendet. Die Untersuchung erfolgt dabei nach den drei vorgenannten Zielen. Basierend auf den Untersuchung im Rahmen dieser Arbeit wurden fünf Änderungen am Linux-Kern seitens des Autors dieser Arbeit erstellt und durch die Entwicklergemeinde akzeptiert. Eine weitere Änderung wurde bereits für gut befunden, aber noch nicht akzeptiert. Die Ergebnisse dieser Arbeit führten ebenfalls zu einer Änderung an der Sperren-Dokumentation im FreeBSD-Kern. Außerdem wurde ein Synchronisationsfehler in FreeBSD aufgedeckt.