一句话：提出松弛操作语义 TMS2-ra，与 RC11 集成，给出验证逻辑 TARO 和 C11 实现 TML-ra，并在 Isabelle/HOL 中验证。
事务内存（TM）在松弛内存模型（如 C11）下缺乏严格基础，难以支持可验证实现。本文提出 TMS2-ra：一个松弛的操作式事务内存规格，并将其与 RC11（修复后的 C11 内存模型）集成，为 TM 库及其客户端提供形式语义。作者定义验证逻辑 TARO，用于证明使用 TMS2-ra 同步的客户端程序，并给出 C11 库 TML-ra，仅用 relaxed 与 release-acquire 原子操作实现 TMS2-ra 所需的同步性质。TML-ra 在 STAMP 基准上优于顺序一致版本；其正确性通过基于模拟的验证技术证明，整个开发在 Isabelle/HOL 中机器化。
Transactional memory (TM) is an intensively studied synchronisation paradigm with many proposed implementations in software and hardware, and combinations thereof. However, TM under relaxed memory, e.g., C11 (the 2011 C/C++ standard) is still poorly understood, lacking rigorous foundations that support verifiable implementations. This paper addresses this gap by developing TMS2-ra, a relaxed operational TM specification. We integrate TMS2-ra with RC11 (the repaired C11 memory model that disallows load-buffering) to provide a formal semantics for TM libraries and their clients. We develop a logic, TARO, for verifying client programs that use TMS2-ra for synchronisation. We also show how TMS2-ra can be implemented by a C11 library, TML-ra, that uses relaxed and release-acquire atomics, yet guarantees the synchronisation properties required by TMS2-ra. We benchmark TML-ra and show that it outperforms its sequentially consistent counterpart in the STAMP benchmarks. Finally, we use a simulation-based verification technique to prove correctness of TML-ra. Our entire development is supported by the Isabelle/HOL proof assistant.
@article{paperbot1433,
title = {Implementing and verifying release-acquire transactional memory in C11},
author = {Sadegh Dalvandi and Brijesh Dongol},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {OOPSLA2},
year = {2022},
doi = {10.1145/3563352}
}