Property-based Testing of Concurrent Lock-free Data Structures

Paulo Sousa

November 2025

---

Abstract

Property based testing (PBT) is a testing methodology that involves automatically checking formal specifications against randomly generated test data. This dissertation describes an experiment of using PBT to test a concurrent lock-free data structure implemented in C using the Haskell QuickCheck library. The approach consists of modeling the data structure throught purely-functional transitions on a state-machine that is then run against a concurrent execution of the real implementation. Runs that cannot be explained by linearization into the purely-functional model correspond to faults in the implementation (i.e. non-atomic operations). We present the testing framework, the data structure and the functional model, and some experimental results.

Bibtex

@MastersThesis{sousa-msc,
  author =  {P. Sousa},
  title =   {{Property-based Testing of Concurrent Lock-free Data Structures}},
  school =  {University of Porto},
  address = {Portugal},
  month =   {November},
  year =    {2025},
  type =    {{MSc Thesis}},
}

Download Thesis

PDF file