一句话：将 SCAR 抽象精化扩展到 TSO/PSO 弱内存模型，显著提升多线程程序验证效率。
本文研究弱内存模型（WMM）下多线程程序的验证问题。现有基于调度约束的抽象精化（SCAR）方法在顺序一致性（SC）下高效，但难以直接处理 TSO、PSO 等 WMM 中同一线程内存操作的非确定性执行。作者将 SCAR 扩展至 WMM，丰富了反例的事件顺序图（EOG）以刻画 SC 与 WMM 下的顺序约束，并提出统一的 EOG 生成方法，可高效获得最小 EOG。在大量多线程 C 程序上的实验表明，该方法显著优于当前先进工具，且在 TSO/PSO 下的验证时间与内存开销与 SC 大致相当。
Scheduling constraint based abstraction refinement (SCAR) is one of the most efficient methods for verifying programs under sequential consistency (SC). However, most multi-processor architectures implement weak memory models (WMMs) in order to improve the performance of a program. Due to the nondeterministic execution of those memory operations by the same thread, the behavior of a program under WMMs is much more complex than that under SC, which significantly increases the verification complexity. This paper elegantly extends the SCAR method to WMMs such as TSO and PSO. To capture the order requirements of an abstraction counterexample under WMMs, we have enriched the event order graph (EOG) of a counterexample such that it is competent for both SC and WMMs. We have also proposed a unified EOG generation method which can always obtain a minimal EOG efficiently. Experimental results on a large set of multi-threaded C programs show promising results of our method. It significantly outperforms state-of-the-art tools, and the time and memory it required to verify a program under TSO and PSO are roughly comparable to that under SC.
DOI 原文 ·
@inproceedings{paperbot4751,
title = {Scheduling constraint based abstraction refinement for weak memory models},
author = {Liangze Yin and Wei Dong and Wanwei Liu and Ji Wang},
booktitle = {ASE},
year = {2018},
doi = {10.1145/3238147.3238223}
}