一句话：针对 RC11 弱内存模型给出操作语义与通用库正确性条件，使客户端可用规范代码推理程序行为。
并发数据结构与同步机制是模块化软件开发的基础，但在弱内存并发下，库抽象问题——即客户端能否借助简化的规范代码推理程序行为——一直缺乏通用解答。本文针对 RC11 内存模型的一个片段，给出与之等价的操作语义表示，显式暴露线程间的知识传播，并足以将库行为刻画为全序的操作执行轨迹；据此提出通用的库正确性条件。作者还引入新的访问模式（access modes），用以精确描述库内部不暴露给客户端的同步，以及库对客户端外部同步提出的要求。文章通过多个性质各异的实例展示了该方法的适用性。
Concurrent data structures and synchronization mechanisms implemented by expert developers are indispensable for modular software development. In this paper, we address the fundamental problem of library abstraction under weak memory concurrency, and identify a general library correctness condition allowing clients of the library to reason about program behaviors using the specification code, which is often much simpler than the concrete implementation. We target (a fragment of) the RC11 memory model, and develop an equivalent operational presentation that exposes knowledge propagation between threads, and is sufficiently expressive to capture library behaviors as totally ordered operational execution traces. We further introduce novel access modes to the language that allow intricate specifications accounting for library internal synchronization that is not exposed to the client, as well as the library's demands on external synchronization by the client. We illustrate applications of our approach in several examples of different natures.
@article{paperbot2064,
title = {An Operational Approach to Library Abstraction under Relaxed Memory Concurrency},
author = {Abhishek Kr Singh and Ori Lahav},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {POPL},
year = {2023},
doi = {10.1145/3571246}
}