多副本原子语义下 C/C++11 并发程序的动态验证
编程语言
2021-05-28 v2
摘要
我们研究了在多副本原子(Multi-Copy-Atomic, MCA)语义下对 C11 程序进行运行时分析的问题。在 MCA 下,可以仅通过线程事件的交错与重排来分析程序执行结果,因此直观地解释程序结果变得简单。较新版本的 ARM(ARMv8 及以后)、Alpha 以及 Intel 的 x86 均支持 MCA。我们的测试表明,最先进的动态验证技术在 C11 内存模型下分析程序执行时,会产生在 MCA 语义下可解释为误报的安全性属性违例。区分真实与虚假违例给用户带来了不必要的负担。在本工作中,我们提供了一种动态验证技术(MoCA),用于分析在 MCA 模型下被允许的 C11 程序执行。我们设计了一种 happens-before 关系并引入一致性规则,以精确刻画那些在 MCA 模型下被允许的 C11 程序执行。MoCA 对状态空间的探索基于最先进的动态验证算法 source-DPOR。我们的实验证实,MoCA 捕获了所有一致的 C11 程序执行,并且对 MCA 模型是精确的。
引用
@article{arxiv.2103.01553,
title = {Dynamic Verification of C/C++11 Concurrency over Multi Copy Atomics},
author = {Sanjana Singh and Divyanjali Sharma and Subodh Sharma},
journal= {arXiv preprint arXiv:2103.01553},
year = {2021}
}
备注
12 pages of main paper + 2 5 pages of appendix and 19 figures