References & Citations
Computer Science > Programming Languages
Title: Model Checking Race-freedom When "Sequential Consistency for Data-race-free Programs" is Guaranteed
(Submitted on 29 May 2023 (v1), last revised 20 Jul 2023 (this version, v2))
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.
Submission history
From: Stephen Siegel [view email][v1] Mon, 29 May 2023 16:52:36 GMT (142kb)
[v2] Thu, 20 Jul 2023 17:45:38 GMT (141kb)
Link back to: arXiv, form interface, contact.