Algorithmische Analyse von nebenläufigen Systemen

Computersysteme sind heutzutage allgegenwärtig. Auf der einen Seite, übernimmt Software ständig neue, kritische Aufgaben, von Systemen für medizinische Assistenz bis zu selbstfahrenden Autos. Auf der anderen Seite, ist Software zu einem unverzichtbaren Teil unseres Alltags geworden, beispielsweise bei Kommunikationsdiensten, Smart-Home-Geräten, E-Business und Online-Banking-Transaktionen. Die zunehmende Nachfrage nach computergestützter Automatisierung bedingt die Notwendigkeit von formaler Verifikation. Es gibt immer die Möglichkeit eines Systemversagens, und je mehr die Gesellschaft auf diese Systeme angewiesen ist, desto schlimmer sind die Folgen des Versagens. Programmanalyse und verifikation ermöglichen es auf systematische Weise die Korrektheit von Programmen zu zeigen, und Programmfehler in einem frühen Entwicklungsstadium zu entdecken. Die Mehrheit der heutigen Systeme ist nebenläufig, bedingt durch Fortschritt in der Hardwareentwicklung von Multicore-Architekturen und durch dem zunehmenden Erfolg von Cloud-basierten Diensten. ine der größten Herausforderungen der Softwareentwicklung ist die Verifikation von nebenläufigen Programmen. Einerseits sind solche Programme aufgrund der inhärenten Komplexität, die sich aus den Wechselwirkungen der nebenläufigen Komponenten ergibt, notorisch schwierig korrekt zu schreiben. Andererseits ist ein fehlerhaftes Verhalten durch Tests schwer reproduzierbar, so dass man auf systematisches (formales) Beweisen angewiesen ist um die Korrektheit des Programms zu zeigen. Obwohl die nebenläufige Programmierung immer wichtig wird, sind noch viele Herausforderungen der nebenläufige Verifikation ungelöst. Darunter ist die Skalierbarkeit wohl das größte Problem: Wie können wir der exponentiellen Komplexitätssteigerung aufgrund des nebenläufigen Nicht-Determinismus Herr werden? Versuche der Komplexität mittels Optimierungen in der Software Herr zu werden sind nicht zielführend. Solche Versuche führen oft nur zu inkrementellen Verbesserungen, es fehlt eine solide theoretische Grundlage und ein genereller Ansatz. Zusätzlich entstehen durch die ständige Weiterentwicklung von nebenläufigen Systemen andauernd neue Herausforderungen, wie zum Beispiel verbesserte Kommunikationsmethoden und Verzögerungen bei der Synchronisation. Diese Herausforderungen dürfen nicht ungelöst bleiben. Es bedarf grundlegender Fortschritte damit die nebenläufige Verifikation praktisch anwendbar ist. Mein Vorschlag besteht darin, die Grundlagen der formale Verifikation von nebenläufigen Systemen zu studieren. Das Hauptziel ist neue Theorien und Algorithmen zu entwickeln, und das sekundäre Ziel ist die Entwicklung von neuen Tools, die auf den neuen Algorithmen aufbauen. Im Vergleich zu bestehenden Engineering Techniken, hat dieser Ansatz zwei Vorteile: Zum Ersten führt ein algorithmischer Ansatz zu starken, beweisbaren Garantien, die die neuen Methoden universell anwendbar machen. Zum Zweiten erfordern gute Algorithmen auch gute Theoreme um die Intuition zu formalisieren. Dies ist der beste Weg, damit der Bereich auf eine stabile Weise, über die inkrementellen Verbesserungen von Ad-hoc-Lösungen hinaus, vorankommen kann. Ein solcher Paradigmenwechsel wird eine solide Basis für neue Werkzeuge bieten, deren Anwendbarkeit über die inkrementelle Verbesserungen der technischen Implementierung allein, hinausgeht.

Das Projekt hat zu neue Methodologien in drei verschiedeneBereichen der Programmanalyse beitragt. Diese werden im Folgenden kurz beschrieben. Erstens, haben wir neue, effiziente Algorithmen zur Analyse des Speicherbedarfs von Programmen entwickelt. Der Speicherbedarf bezieht sich auf das Pattern der Speicherzugriffe, die ein Programm durchführt. Durch die Analyse dieses Patterns können wir die Speicherzugriffe, die von das Programm in der Zukunft vornehmen werden, vorhersagen und die Daten proaktiv abrufen, bevor sie, zum Beispiel, angefordert werden. Dieser Prozess führt zu einer Leistungsoptimierung, da das Programm einen direkten Zugriff auf die Daten hat, ohne lange Wartezeiten für die Datenübertragung von dem Speicher zu der CPU. Das Problem der Analyse des Speicherfootprints ist generell bekannt als ein unlenksames Problem zu sein. Im Rahmen unseres Projekts haben wir große Klassen von komplexen Programmen, wie zum Beispiel numerische Berechnungsprograme, identifiziert, für denen schnelle Algorithmen entwickelt konnten, wobei wir die bekannten schwerfälligen Ergebnisse für den allgemeinen Fall umgegangen haben. Zweitens, haben wir neue Algorithmen für die effiziente Verifikation von nebenläufigen Systeme entwickelt. Ein nebenläufiges System ist bekanntlich schwer zu analysieren, da es aufgrund des Zusammenwirkens seiner Komponenten ein unberechenbares Verhalten ausstellen kann. Das macht die Analyse der nebenläufigen Systeme zu einer ständigen Herausforderung. Im Rahmen unseres Projekts haben wir einen neuen Algorithmus entwickelt, der in der Lage ist, innerhalb berechtigten Zeitraum komplexere nebenläufige Programme als die bestehenden Techniken zu analysieren. Drittens, haben wir neue Algorithmen für die effiziente prädiktive Prüfung der nebenläufigen Systeme entwickelt. In Allgemeinen beschäftigt sich der Bereich der prädiktiven Prüfung mit der folgender Herausforderung: wenn wir die Ausführung eines nebenläufiges Programmes beobachten, bei der kein Fehler auftritt, können wir dann erkennen, ob eine andere ähnliche Ausführung zu einem Fehler führen würde? Obwohl dieser Ansatz im Allgemeinen keine Garantie für die Erkennung von Fehlern bietet, wird er häufiger verwendet als die Verifizierung von nebenläufigen Systemen, weil er in der Praxis aufgrund zeitlicher Beschränkungen leichter durchführbar ist. Im Rahmen unseres Projekts haben wir einen neuen, schnellen Algorithmus für die prädiktive Prüfung der nebenläufigen Systeme entwickelt. Im Vergleich zu bestehenden Techniken ist unser Algorithmus in der Lage den Begriff der Ähnlichkeit in Bezug auf die Referenzausführung zu entspannen und damit mehr Fehler als die bestehenden Techniken zu erkennen. Der Algorithmus wurde auf große und komplexe Programme angewendet und war in der Lage verschiedene Fehler zu erkennen, die schon existieren aber bisher unentdeckt geblieben waren.