Verfication of concurrent programs in weak memory models

Abstract

Moderne Processoren nutzen schwache Speichermodelle, um die Ausführung von Code zu optimieren. Im Vergleich zu sequentiell konsistenten Speichermodellen erlauben schwache Speichermodelle die Umordnung von Codeanweisungen. Während dies das Verhalten eines Single-Thread-Programmes nicht verändert, kann es in Multicore-Systemen Fehler verursachen indem Ausführungsreihenfolgen zwischen Threads ermöglicht werden, die ansonst nicht möglich wären.Diese Fehler sind für Entwickler oft schwer zu erkennen und zu verstehen.Diese Thesis schlägt vor, mithilfe von Kronecker Algebra mögliche Ausführungsreihenfolgen von Multithread-Programmen innerhalb schwacher Speichermodelle zu modellieren. Dies kann dann verwendet werden, um Race Conditions im System zu erkennen. Der Fokus liegt dabei speziell auf schwachen Speichermodellen die Release-Acquire Semantiken nutzen. Im Rahmen der Arbeit wird ein Prototyp entwickelt, der das System zur Erkennung von Race Conditions in Multithread-Programmen einzusetzen, die in LLVM-Bytecode kompiliert wurden, um zu zeigen, dass das System in der Lage ist, in Programmen Probleme zu identifizieren, die unter Verwendung von Release-Acquire Speichermodellen auftreten, obwohl das Programm unter sequentiellen Speichermodellen korrekt war. Der Prototyp bewies die Korrektheit der sequentiellen Versionen von Petersons und Dekker's Algorithmus und erkannte auch die Fehler, die auftreten, wenn sie nahezu unverändert unter der Verwendung von Release-Acquire-Speichermodellen ausgeführt werden.

Modern Central Processing Units (CPUs) utilize weak memory models to optimize code execution. Compared to sequential consistent memory models, weak memory models allow the reordering of code instructions. While this does not alter the behavior of a single-thread program, it can cause bugs in multicore systems by allowing execution orders between threads that would otherwise not be possible. These errors are often problematic for the developer to detect and understand. This thesis proposes to use Kronecker Algebra to model possible execution orders of multithreaded programs within weak memory models.The output of such a toolchain can then be used to detect race conditions within the system.It focuses explicitly on weak memory models using release-acquire semantics. Alongside the thesis, a prototype is developed for the proposed system to detect race conditions in multithreaded programs compiled into LLVM-bytecode.This is done to show that the system can detect problems caused when running a program using release-acquire memory models. However, the program was correct under sequential memory models. The prototype correctly proved the correctness of the sequential versions of Peterson's and Dekker's Algorithm. Moreover, the prototype detected the errors that arise when Peterson's and Dekker's Algorithms run without modifications using release-acquire memory models.