Algorithmische Analyse von nebenlÀufigen Systemen
Algorithmic Analysis of Concurrent Systems
Wissenschaftsdisziplinen
Informatik (100%)
Keywords
-
Software Verification,
Concurrency,
Algorithms,
St
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.
Research Output
- 219 Zitationen
- 6 Publikationen
-
2020
Titel Limits on amplifiers of natural selection under death-Birth updating DOI 10.1371/journal.pcbi.1007494 Typ Journal Article Autor Tkadlec J Journal PLOS Computational Biology Link Publikation -
2019
Titel Population structure determines the tradeoff between fixation probability and fixation time DOI 10.1038/s42003-019-0373-y Typ Journal Article Autor Tkadlec J Journal Communications Biology Seiten 138 Link Publikation -
2019
Titel Faster Algorithms for Dynamic Algebraic Queries in Basic RSMs with Constant Treewidth DOI 10.1145/3363525 Typ Journal Article Autor Chatterjee K Journal ACM Transactions on Programming Languages and Systems (TOPLAS) Seiten 1-46 -
2019
Titel Fast, sound, and effectively complete dynamic race prediction DOI 10.1145/3371085 Typ Journal Article Autor Pavlogiannis A Journal Proceedings of the ACM on Programming Languages Seiten 1-29 Link Publikation