一句话：提出观测鲁棒性，将 C11 风格内存模型下的并发程序鲁棒性验证归约为顺序一致性下的可达性问题。
包含 relaxed 访问以及 release/acquire 访问与栅栏的 C11 风格内存模型，其弱内存行为使并发程序验证十分困难。本文研究该模型下的鲁棒性验证：判断程序在弱内存模型下的行为是否与顺序一致（SC）语义一致。作者证明该问题可归约为 SC 下的标准可达性问题，从而复用成熟的验证技术。针对已有鲁棒性概念无法处理序列锁等使用推测读的程序，论文提出新的“观测鲁棒性”性质并给出可靠的检查方法。作者实现了原型工具并应用于多个具有挑战性的并发算法，是首个面向包含 relaxed 访问与 release/acquire 栅栏的并发模型的鲁棒性验证方法。
We study the problem of verifying the robustness of concurrent programs against a C11-style memory model that includes relaxed accesses and release/acquire accesses and fences, and show that this verification problem can be reduced to a standard reachability problem under sequential consistency. We further observe that existing robustness notions do not allow the verification of programs that use speculative reads as in the sequence lock mechanism, and introduce a novel "observational robustness" property that fills this gap. In turn, we show how to soundly check for observational robustness. We have implemented our method and applied it to several challenging concurrent algorithms, demonstrating the applicability of our approach. To the best of our knowledge, this is the first method for verifying robustness against a programming language concurrency model that includes relaxed accesses and release/acquire fences.
@article{paperbot1164,
title = {Verifying observational robustness against a c11-style memory model},
author = {Roy Margalit and Ori Lahav},
journal = {Proceedings of the ACM on Programming Languages},
volume = {5},
number = {POPL},
year = {2021},
doi = {10.1145/3434285}
}