基于观测等价性的C/C++并发动态验证
编程语言
2022-08-02 v3 分布式、并行与集群计算
摘要
在松弛内存模型（rmm）语义下的程序执行分析难度显著增大；rmm语义导致程序事件乱序执行，从而引发状态空间爆炸。动态偏序归约（DPOR）是解决此类状态空间爆炸的一种强有力技术，已被用于验证 TSO、PSO 和 POWER 等 rmm 下的程序。此类 DPOR 技术的核心概念是迹等价，其基于程序事件间的独立关系计算。我们提出了一种更粗粒度的、感知 rmm 的迹等价概念，称为观测等价性（OE）。若两个程序行为中每个读事件都读取相同的值，则它们是观测等价的。我们提出观测独立性（OI）的概念，并给出一种算法构造以高效计算（模 OI 的）迹等价。我们还通过首先提供精细的 happens-before（hb）关系来刻画 C/C++ 并发语义，从而展示了带 OE 的 DPOR 在线程化 C/C++ 程序上的有效性。我们在名为 Drista 的运行时模型检测器中实现了所提技术。我们的实验表明：（i）与现有非 OE 技术相比，我们在 OE 下探索的迹数量上实现了显著节省；（ii）我们对 C/C++ 并发的处理比现有最先进技术更为广泛。
引用
@article{arxiv.1905.03957,
title = {Dynamic Verification with Observational Equivalence of C/C++ Concurrency},
author = {Sanjana Singh and Divyanjali Sharma and Subodh Sharma},
journal= {arXiv preprint arXiv:1905.03957},
year = {2022}
}
备注
The claims in the paper are incorrect. The claims have been corrected in arXiv:2103.01553