K Struct. Ein Ansatz zur Analyse und Beschreibung von Nebenläufigkeit in Betriebssystemen

Der Paradigmenwechsel bei der Architektur von Prozessoren hin zu Mehrkernprozessoren (multicore processor) verlangt von Software ein erhöhtes Maß an Nebenläufigkeit, um die verfügbaren parallelen Rechenressourcen effizient zu nutzen. Betriebssysteme sind ein Beispiel für Software, die hochgradig asynchron und damit in hohem Maße nebenläufig ist. Wird in einer solchen Software das Konzept des gemeinsamen Hauptspeichers (shared memory) zur Kommunikation zwischen einzelnen Aktivitäten verwendet, müssen Zugriffe auf diese nicht-skalaren Daten in kritischen Abschnitten erfolgen, die geeignet synchronisiert werden. Für das Überwachen und Beobachten des Systems ist häufig ein Zugriff auf nicht-skalare Daten im gemeinsamen Speicher notwendig, die den Zustand des Systems beschreiben. Ohne eine Beachtung des Protokolls, das zur Synchronisation verwendet wird, besteht die Gefahr, dass ein solches Überwachungswerkzeug Daten ausliest, die inkonsistent sind und keinen tatsächlichen Zustand des Systems repräsentieren. Mit dem Vorhandensein vieler paralleler Ausf¨uhrungseinheiten nimmt die Gefahr von Wettlaufsituationen zwischen Betriebssystem und Beobachtungswerkzeug und damit die Gefahr des Auslesens von inkonsistenten Daten zu. Um diese Probleme zu vermeiden, wird in der vorliegenden Arbeit der KStruct-Ansatz vorgestellt, der es einem dynamischen, nicht-integrierten Beobachtungswerkzeug erlaubt, auf den Zustand eines Betriebssystems unter Berücksichtigung des Synchronisationsprotokolls zuzugreifen. Dazu wird mit Hilfe der Sprache KStruct Access, einer Erweiterung der Programmiersprache C, das Synchronisationsprotokoll des Betriebssystems definiert, welches als Vertrag zwischen Betriebssystem und Überwachungswerkzeug dient. Die Annotationen werden von einem Compiler in eine Komponente übersetzt, die von Beobachtungswerkzeugen für den Zugriff auf den gemeinsamen Speicher verwendet werden kann, um Daten unter Einhaltung des Protokolls auszulesen. Um den Annotationsprozess gerade für bestehende Softwaresysteme zu unterstützen, wird zusätzlich KStruct Advice vorgestellt, womit sich ein Betriebssystem hinsichtlich des verwendeten Synchronisationsprotokolls analysieren lässt. Dazu wird ein formales Modell einer Sperre definiert, welches die Grundlage für eine statische Datenflussanalyse zur Berechnung der Zustände aller Sperren darstellt. Der Zustand einer Sperre wird schließlich mit Zugriffen auf Datenstrukturen im gemeinsamen Speicher korreliert und so ein Synchronisationsprotokoll abgeleitet. Die Ergebnisse des Ansatzes werden im Kontext des Windows Research Kernels betrachtet, diskutiert und evaluiert. The paradigm shift in the design and the architecture of computer processors from uniprocessors to multicore processors imposes a demand for concurrency in software systems to efficiently leverage the existence of multiple compute resources. An operating system is an example for such a concurrent software system, which reacts concurrently to asynchronously occurring events. If such a software system makes use of shared memory to communicate among its threads, accesses to non-scalar data must be synchronized appropriately. For the purpose of monitoring and tracing events in such a system, there is usually the need to access non-scalar data on the shared memory. Without the application of the appropriate concurrency control protocol, which is used to implement mutual exclusion on critical sections, the monitoring or tracing tool, there is the risk to retrieve inconsistent data that represents no actual state at all. Due to the increasing number of parallel processors per computer system, the probability of race conditions between the system under investigation and the monitoring tool may rise as well. This also includes the risk of accessing data inconsistently. To remedy those issues, this thesis presents the KStruct-Approach, which allows a non-integrated monitoring or tracing tool to access the shared state of an operating system consistently, by complying to the system’s concurrency control protocol. This is achieved by two means. First the language KStruct Access is defined, which is an extension to the C programming language. This language allows for the specification of the concurrency control protocol by annotating data structures, which then serves as the contract between the operating system and the monitoring tool. Second, a compiler is implemented to leverage those annotations for generating a component, which may be used by arbitrary monitoring applications and which guarantees concurrency control protocol compliance for the specified system. Thus, KStruct achieves consistent accesses to the shared state of the operating system. In order to support the annotation process, this thesis presents KStruct Advice, which analyzes an operating system with respect to the applied concurrency control protocol. Therefore, a formal model of a lock and operations on this lock are defined. This model is used for a static data fl