Property-Based Testing of a Concurrent Lock-Free Data Structure

Paulo Sousa, Ricardo Rocha and Pedro Vasconcelos

September 2025

---

Abstract

Property-based testing (PBT) is a testing methodology that involves automatically checking formal specifications against randomly generated test data. This paper 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 through 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

@InProceedings{sousa-inforum25,
  author =    {P. Sousa and R. Rocha and P. Vasconcelos},
  title =     {{Property-Based Testing of a Concurrent Lock-Free Data Structure}},
  booktitle = {16th INForum - Simpósio de Informática (INForum 2025)},
  editor =    {F. Araújo and E. Ribeiro},
  month =     {September},
  year =      {2025},
  address =   {Évora, Portugal},
}

Download Paper

PDF file