论文标题
实施和验证发行速度交易记忆（扩展版本）
Implementing and Verifying Release-Acquire Transactional Memory (Extended Version)
论文作者
论文摘要
交易内存（TM）是一个深入研究的同步范式，其中有许多在软件和硬件中的实现及其组合。但是，在轻松的内存下，例如C11（2011 C/C ++标准）仍然对TM缺乏支持可验证的实现的严格基础。本文通过开发TMS2-RA（一种放松的操作TM规范）来解决这一差距。我们将TMS2-RA与RC11（已修复的C11内存模型）集成在一起，以为TM库及其客户提供正式的语义。我们开发了一种逻辑，用于验证使用TMS2-RA进行同步的客户端程序。我们还展示了如何通过使用放松和发行的原子原子的C11库TMLA库来实现TMS2-RA，但可以保证TMS2-RA所需的同步属性。我们基于TML-RA进行基准测试，并表明它的表现优于其在邮票基准测试中的依次一致性。最后，我们使用基于仿真的验证技术来证明TML-RA的正确性。 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.
