Model Checking Race-freedom When "Sequential Consistency for Data-race-free Programs" is Guaranteed
Model Checking Race-freedom When "Sequential Consistency for Data-race-free Programs" is Guaranteed
复制标题
当“无数据竞争程序的顺序一致性”得到保证时，模型检查无竞争
DOI：
10.48550/arxiv.2305.18198
复制
发表时间：
2023
期刊：
影响因子：
--
通讯作者：
Stephen F. Siegel
中科院分区：
文献类型：
--
作者：
Wen;J. Hückelheim;P. Hovland;Ziqing Luo;Stephen F. Siegel
许多并行编程模型保证，如果程序的所有顺序一致（SC）执行都没有数据竞争，那么程序的所有执行将看起来是顺序一致的。这大大简化了程序的推理，但留下了如何验证所有SC执行都是无种族的问题。在本文中，我们表明，与一些简单的修改，模型检测可以是一个有效的工具，用于验证种族自由。我们探索这种技术的一套C程序并行与OpenMP。
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.
影响因子：
1.3
作者：
Betts A
通讯作者：
Betts A