VSL Publications

Model Checking Race-freedom when “Sequential Consistency for Data-Race-Free Programs” is Guaranteed

Cite
Wenhao Wu, Jan Hückelheim, Paul D. Hovland, Ziqing Luo, and Stephen F. Siegel. Model Checking Race-freedom when “Sequential Consistency for Data-Race-Free Programs” is Guaranteed. Computer Aided Verification (CAV 2023), Lecture Notes in Computer Science 13965, pp. 265--287, Springer, Cham, 2023.
Abstract
Many parallel programming models guarantee that if all sequentially consistent (SC) executions of a program are free of data races, then all executions of the program will appear to be sequentially consistent. This greatly simplifies reasoning about the program, but leaves open the question of how to verify that all SC executions are race-free. In this paper, we show that with a few simple modifications, model checking can be an effective tool for verifying race-freedom. We explore this technique on a suite of C programs parallelized with OpenMP.
Downloads
  1. sc4drf.pdf (extended version)
Related Links
  1. Published version
  2. Preprint on arXiv (extended version)
  3. Experimental artifacts (GitHub)
BibTeX 
@InProceedings{wu-etal:2023:sc4drf,
  author = {Wu, Wenhao and H{\"u}ckelheim, Jan and Hovland, Paul
                  D. and Luo, Ziqing and Siegel, Stephen F.},
  editor = {Enea, Constantin and Lal, Akash},
  title = {Model Checking Race-Freedom When ``Sequential Consistency
                  for Data-Race-Free Programs'' is Guaranteed},
  booktitle = {Computer Aided Verification},
  series = {Lecture Notes in Computer Science},
  volume = {13965},
  doi = {10.1007/978-3-031-37703-7_13},
  year = {2023},
  publisher = {Springer},
  address = {Cham},
  pages = {265--287}
}
VSL | Publications