TU Darmstadt / ULB / TUprints

Verification and Enforcement of Safe Schedules for Concurrent Programs

Metzler, Patrick (2020)
Verification and Enforcement of Safe Schedules for Concurrent Programs.
Technische Universität Darmstadt
doi: 10.25534/tuprints-00013432
Ph.D. Thesis, Primary publication, Publisher's Version

[img]
Preview
Text
Dissertation-Metzler.pdf
Copyright Information: In Copyright.

Download (1MB) | Preview
Item Type: Ph.D. Thesis
Type of entry: Primary publication
Title: Verification and Enforcement of Safe Schedules for Concurrent Programs
Language: English
Referees: Peters, Prof. Dr. Kirstin ; Weissenbacher, Prof. Dr. Georg
Date: 2020
Place of Publication: Darmstadt
Collation: vii, 124 Seiten
Date of oral examination: 24 April 2020
DOI: 10.25534/tuprints-00013432
Abstract:

Automated software verification can prove the correctness of a program with respect to a given specification and may be a valuable support in the difficult task of ensuring the quality of large software systems. However, the automated verification of concurrent software can be particularly challenging due to the vast complexity that non-deterministic scheduling causes.

This thesis is concerned with techniques that reduce the complexity of concurrent programs in order to ease the verification task. We approach this problem from two orthogonal directions: state space reduction and reduction of non-determinism in executions of concurrent programs.

Following the former direction, we present an algorithm for dynamic partial-order reduction, a state space reduction technique that avoids the verification of redundant executions. Our algorithm, EPOR, eagerly creates schedules for program fragments. In comparison to other dynamic partial-order reduction algorithms, it avoids redundant race and dependency checks. Our experiments show that EPOR runs considerably faster than a state-of-the-art algorithm, which allows in several cases to analyze programs with a higher number of threads within a given timeout.

In the latter direction, we present a formal framework for using incomplete verification results to extract safe schedulers. As incomplete verification results do not need to proof the correctness of all possible executions of a program, their complexity can be significantly lower than complete verification results. Hence, they can be faster obtained. We constrain the scheduling of programs but not their inputs in order to preserve their full functionality. In our framework, executions under the scheduling constraints of an incomplete verification result are safe, deadlock-free, and fair. We instantiate our framework with the Impact model checking algorithm and find in our evaluation that it can be used to model check programs that are intractable for monolithic model checkers, synthesize synchronization via assume statements, and guarantee fair executions.

In order to safely execute a program within the set of executions covered by an incomplete verification, scheduling needs to be constrained. We discuss how to extract and encode schedules from incomplete verification results, for both finite and infinite executions, and how to efficiently enforce scheduling constraints, both in terms of reducing the time to look up permission of executing the next event and executing independent events concurrently (by applying partial-order reduction).

A drawback of enforcing scheduling constraints is a potential overhead in the execution time. However, in several cases, constrained executions turned out to be even faster than unconstrained executions. Our experimental results show that iteratively relaxing a schedule can significantly reduce this overhead. Hence, it is possible to adjust the incurred execution time overhead in order to find a sweet spot with respect to the amount of effort for creating schedules (i.e., the duration of verification). Interestingly, we found cases in which a much earlier reduction of execution time overhead is obtained by choosing favorable scheduling constraints, which suggests that execution time performance does not simply rely on the number of scheduling constraints but to a large extend also on their structure.

Alternative Abstract:
Alternative AbstractLanguage

Automatisierte Softwareverifikation erlaubt es, die Korrektheit eines Programms in Bezug auf eine gegebene Spezifikation zu beweisen und kann somit eine wertvolle Unterstützung bei der schwierigen Aufgabe der Qualitätssicherung großer Softwaresysteme sein. Jedoch stellt die zusätzliche Komplexität nichtdeterministischen Schedulings eine besondere Herausforderung für die automatisierte Verifikation nebenläufiger Software dar.

Diese Dissertation befasst sich mit Techniken zur Reduktion der Komplexität nebenläufiger Programme, um das Verifikationsproblem zu erleichtern. Wir erarbeiten dazu Lösungen aus zwei unterschiedlichen Richtungen: Zustandsraumreduktion und Reduktion von Nichtdeterminismus in Ausführungen nebenläufiger Programme.

Ersterer Richtung folgend stellen wir einen Algorithmus für Dynamic-Partial-Order-Reduction vor, einer Zustandsraumreduktion, die die Verifikation redundanter Ausführungen vermeidet. Unser Algorithmus, EPOR, erzeugt begierig (eager) Schedules für Programmfragmente. Im Vergleich zu anderen Algorithmen für Dydamic-Partial-Order-Reduction vermeidet er redundante Race- und Abhängigkeitstests. Unsere Experimente zeigen, dass EPOR deutlich schneller als ein bekannter und aktueller Algorithmus läuft, was in mehreren Fällen die Verifikation von Programmen mit mehr Threads innerhalb einer gegebenen Zeit erlaubt.

In letzterer Richtung stellen wir ein formales Framework zur Nutzung von unvollständigen Verifikationsergebnissen zur Erstellung von sicheren Schedules vor. Da unvollständige Verifikationsergebnisse nicht die Korrektheit aller möglichen Ausführungen eines Programms beweisen müssen, kann ihre Komplexität deutlich niedriger als bei vollständigen Verifikationsergebnissen sein. Dadurch können sie sehr viel schneller generiert werden. Wir schränken das Scheduling von Programmen ein, jedoch nicht ihre Eingabe, um ihre Funktionalität zu erhalten. In unserem Framework sind Ausführungen innerhalb den Schedulingbeschränkungen eines unvollständigen Verifikationsergebnisses sicher (safe), deadlockfrei und fair. Wir instantiieren unser Framework mit dem Impact Model-Checking-Algorithmus und zeigen in unserer Evaluation, dass es genutzt werden kann um Programme zu verifizieren, die nicht durch monolithisches Model-Checking handhabbar sind, um Synchronisation durch assume-Statements zu synthetisieren und um faire Ausführungen zu garantieren.

Um ein Programm sicher innerhalb der durch ein unvollständiges Verifikationsergebnisses abgedeckten Ausführungen auszuführen, muss das Scheduling beschränkt werden. Wir diskutieren, wie aus unvollständigen Verifikationsergebnissen Schedules extrahiert und encodiert werden können, sowohl für endliche als auch für unendliche Ausführungen. Zusätzlich diskutieren wir, wie Schedulingbeschränkungen effizient umgesetzt werden können, sowohl im Hinblick auf ein schnelles Nachschlagen der Erlaubnis, das nächste Event auszuführen, als auch auf die nebenläufige Ausführung unabhängiger Events (durch die Anwendung von Partial-Order-Reduction).

Ein Nachteil der Umsetzung von Schedulingbeschränkungen ist ein potenzieller Overhead in der Ausführungsdauer, jedoch erwiesen sich beschränkte Ausführungen in mehreren Fällen sogar als schneller als unbeschränkte Ausführungen. Unsere experimentellen Ergebnisse zeigen, dass das iterative Lockern von Schedulingbeschränkungen den Overhead in der Ausführungsdauer reduzieren kann. Daher ist es möglich, den erlittenen Overhead anzupassen, sodass ein optimaler Bereich im Hinblick auf die zur Erzeugung der Schedules nötigen Zeit (also die Dauer der Verifikation) gefunden wird. Interessanterweise zeigen sich Fälle, in denen durch die Wahl geeigneter Schedules der Overhead bereits viel früher reduziert werden kann, was nahelegt, dass die Ausführungsgeschwindigkeit nicht einfach nur von der Anzahl an Schedulingbeschränkungen abhängt, sondern zu einem großen Teil auch von deren Struktur.

German
Status: Publisher's Version
URN: urn:nbn:de:tuda-tuprints-134321
Classification DDC: 000 Generalities, computers, information > 004 Computer science
Divisions: 20 Department of Computer Science > Theory of Parallel Systems
Date Deposited: 11 Dec 2020 14:20
Last Modified: 27 Apr 2023 10:45
URI: https://tuprints.ulb.tu-darmstadt.de/id/eprint/13432
PPN: 473884259
Export:
Actions (login required)
View Item View Item