Analyse expliziter Zustandsverwaltung als Mittel der Synchronisation

Abstract

Parallelität ist fester Bestandteil moderner Softwareentwicklung. Nebenläufige Zugriffe auf geteilte Ressourcen müssen synchronisiert werden, da sonst Softwarefehler wie Data-Races entstehen. Zur Synchronisation werden neben etablierten auch häufig »selbstgestrickte« zustandsbasierte Mechanismen eingesetzt. Diese implementieren oft endliche Automaten. Bestehenden leichtgewichtigen, auf Mustererkennung ausgerichteten Ansätzen zur Analyse von Synchronisationseigenschaften expliziter Zustandsverwaltung fehlt es an Mächtigkeit, um solche Muster befriedigend zu analysieren. Diese Abhandlung stellt einen neuen, deutlich schwergewichtigeren Ansatz zur Analyse expliziter Zustandsverwaltung als Mittel der Synchronisation vor. Dabei reduziert statische Analyse in der Sprache C geschriebene Systeme auf im formalen Prozesskalkül CSP verfasste Modelle. Refinement-Checker untersuchen, ob Paare von Zugriffen auf Variablen im Modell ein Data-Race bilden. Lässt sich das Data-Race im Modell ausschließen, ist es dank konservativer Approximierung auch im ursprünglichen System unerreichbar. Die Modellierung und Vorverarbeitung des Modells wird erläutert. Die Evaluation zeigt, dass der neue Ansatz oft eine bessere Einschätzung der Synchronisationseigenschaften expliziter Zustandsverwaltung liefert als bisherige Ansätze. Die Anwendung auf reale eingebettete Systeme aus Automobilen demonstriert, dass der Ansatz praktisch einsetzbar ist.