dissertation · Research Repository (Delft University of Technology) · 2024

Verifying weak memory concurrent data structure implementations

Henkes, Casper (author)

Cited by 0Open access

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.

Cite this paper

APA 7

Henkes, C. A. (2024). Verifying weak memory concurrent data structure implementations. Research Repository (Delft University of Technology).

MLA 9

Henkes, Casper (author). “Verifying weak memory concurrent data structure implementations.” Research Repository (Delft University of Technology), 2024.

Chicago

Henkes, Casper (author). 2024. “Verifying weak memory concurrent data structure implementations.” Research Repository (Delft University of Technology).

Harvard

Henkes, C.A. (2024) ‘Verifying weak memory concurrent data structure implementations’, Research Repository (Delft University of Technology).

BibTeX

@phdthesis{henkes2024verifying,
  title = {{Verifying weak memory concurrent data structure implementations}},
  author = {Henkes, Casper (author)},
  school = {Research Repository (Delft University of Technology)},
  year = {2024}
}

Made from the index record. Check names, capitalisation and page numbers against the paper. Need another style? AI for Research has over 10,000.