一句话：首次提出面向弱内存模型的动态鲁棒性验证，用位置时钟在 C11 下高效检测程序是否仅表现强一致行为。
标准动态数据竞争检测难以适用于实际弱内存模型：插桩引入额外同步，会掩盖弱一致行为并漏检竞争。本文提出以动态方式验证程序鲁棒性，即确认程序只表现出强一致行为。作者在已有静态判定过程基础上，针对 C11 风格内存模型设计动态鲁棒性验证算法，核心是“位置时钟”（location clocks）——标准竞争检测中向量时钟的变体，从而可按程序有效防御弱内存影响，并与假设强一致的竞争检测结合。作者实现工具 RSan 并在多种设置下评估。据作者所知，这是首个针对弱内存模型的动态鲁棒性验证工作。
Dynamic race detection is a highly effective runtime verification technique for identifying data races by instrumenting and monitoring concurrent program runs. However, standard dynamic race detection is incompatible with practical weak memory models; the added instrumentation introduces extra synchronization, which masks weakly consistent behaviors and inherently misses certain data races. In response, we propose to dynamically verify program robustness —a property ensuring that a program exhibits only strongly consistent behaviors. Building on an existing static decision procedure, we develop an algorithm for dynamic robustness verification under a C11-style memory model. The algorithm is based on “location clocks”, a variant of vector clocks used in standard race detection. It allows effective and easy-to-apply defense against weak memory on a per-program basis, which can be combined with race detection that assumes strong consistency. We implement our algorithm in a tool, called RSan, and evaluate it across various settings. To our knowledge, this work is the first to propose and develop dynamic verification of robustness against weak memory models.
@article{paperbot3098,
title = {Dynamic Robustness Verification against Weak Memory},
author = {Roy Margalit and Michalis Kokologiannakis and Shachar Itzhaky and Ori Lahav},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {PLDI},
year = {2025},
doi = {10.1145/3729277}
}