arXiv Open Access 2023

Model Checking Race-freedom When "Sequential Consistency for Data-race-free Programs" is Guaranteed

Wenhao Wu Jan Hückelheim Paul D. Hovland Ziqing Luo Stephen F. Siegel

Lihat Sumber

Abstrak

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.

Topik & Kata Kunci

cs.PL cs.DC

Penulis (5)

Wenhao Wu

Jan Hückelheim

Paul D. Hovland

Ziqing Luo

Stephen F. Siegel

Format Sitasi

APA MLA BibTeX

Wu, W., Hückelheim, J., Hovland, P.D., Luo, Z., Siegel, S.F. (2023). Model Checking Race-freedom When "Sequential Consistency for Data-race-free Programs" is Guaranteed. https://arxiv.org/abs/2305.18198

Akses Cepat

Lihat di Sumber

Informasi Jurnal

Tahun Terbit: 2023
Bahasa: en
Sumber Database: arXiv
Akses: Open Access ✓