Verifying weak memory concurrent data structure implementations

Verifying weak memory concurrent data structure implementations

Henkes, Casper (TU Delft Electrical Engineering, Mathematics and Computer Science)

Chakraborty, S.S. (mentor)
van Deursen, A. (mentor)
Poulsen, C.B. (graduation committee)

Delft University of Technology

Computer Science

2024-05-14

From formal hardware models to programming language implementations concurrency is everywhere. While there has been a lot of work done on verifying concurrent systems a large part of it is focused on SC. In practice, it is more common to encounter weak memory models for which the techniques developed for SC do not work. There exists previous research on verifying weak memory concurrent programs, however, this work is often limited in scope and is often difficult to understand and apply to a broader context. This thesis gives a general approach for calculating higher-level relations between function calls in a weak memory context that work for weak memory concurrent mutex, stack, and queue data structures. These relations allow us to abstract away implementation details for easier reasoning about program behaviour. These function-level relations and data structure models defined using them are implemented in a stateless model checker and used to verify several existing mutex, stack, and queue implementations.

Weak Memory
Data structures
Verifcation
Stateless Model Checking

http://resolver.tudelft.nl/uuid:5e37b41b-4d51-43b4-a77a-d8aae74a6978

Student theses

master thesis

© 2024 Casper Henkes