Verifying weak memory concurrent data structure implementations
C.L.W. Henkes (TU Delft - Electrical Engineering, Mathematics and Computer Science)
Soham Chakraborty – Mentor (TU Delft - Programming Languages)
Arie Deursen – Mentor (TU Delft - Software Engineering)
C.B. Poulsen – Graduation committee member (TU Delft - Programming Languages)
More Info
expand_more
Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.
Abstract
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.