一句话：提出面向 C11 内存模型的自动化归纳技术，验证并发数据结构库在宽松内存模型下相对顺序一致性的鲁棒性。
并发数据结构库通常用线性化等规格供客户端推理，但高性能实现可能利用宽松内存行为，使客户端推理复杂化。本文不另建宽松内存规格，而是研究库鲁棒性：宽松内存模型下实现的所有行为在顺序一致（SC）下也可发生。作者基于 C11 内存模型鲁棒性工作中在 SC 执行中搜索非鲁棒性见证的思路，建立新的归纳验证技术，利用库的高层 SC 规格（包括线性化）来证明不存在此类见证，从而处理无界并发操作和无界共享位置。该技术具有组合性，可用额外 SC fence 安全保持多个交互库与客户端的鲁棒性。在多个复杂真实库实现上的实验证明了方法的可行性。
Clients reason about the behavior of concurrent data structure libraries such as sets, queues, or stacks using specifications that capture well-understood correctness conditions, such as linearizability. The implementation of these libraries, however, focused as they are on performance, may additionally exploit relaxed memory behavior allowed by the language or underlying hardware that weaken the strong ordering and visibility constraints on shared-memory accesses that would otherwise be imposed by a sequentially consistent (SC) memory model. As an alternative to developing new specification and verification mechanisms for reasoning about libraries under relaxed memory model, we instead consider the orthogonal problem of library robustness , a property that holds when all possible behaviors of a library implementation under relaxed memory model are also possible under SC. In this paper, we develop a new automated technique for verifying robustness of library implementations in the context of a C11-style memory model. This task is challenging because a most-general client may invoke an unbounded number of concurrently executing library operations that can manipulate an unbounded number of shared locations. We establish a novel inductive technique for verifying library robustness that leverages prior work on the robustness problem for the C11 memory model based on the search for a non-robustness witness under SC executions. We crucially rely on the fact that this search is carried out over SC executions, and use high-level SC specifications (including linearizability) of the library to verify the absence of a non-robustness witness. Our technique is compositional - we show how we can safely preserve robustness of multiple interacting library implementations and clients using additional SC fences to guarantee robustness of entire executions. Experimental results on a number of complex realistic library implementations demonstrate the feasibility of our approach.
@article{NagarSCJ24,
title = {Automated Robustness Verification of Concurrent Data Structure Libraries against Relaxed Memory Models},
author = {Kartik Nagar and Anmol Sahoo and Romit Roy Chowdhury and Suresh Jagannathan},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {OOPSLA2},
year = {2024},
doi = {10.1145/3689802}
}