Implementing and Verifying Release-Acquire Transactional Memory (Extended Version)
Implementing and Verifying Release-Acquire Transactional Memory (Extended Version)
复制标题
DOI：
10.48550/arxiv.2208.00315
复制
发表时间：
2022-07
期刊：
影响因子：
--
通讯作者：
Sadegh Dalvandi;Brijesh Dongol
中科院分区：
文献类型：
--
作者：
Sadegh Dalvandi;Brijesh Dongol
transmittance memory（TM）是一种深入研究的同步范例，其中提出了许多软件和硬件及其组合的实现方式。然而，放松记忆下的TM，例如，C11（2011 C/C++标准）仍然知之甚少，缺乏支持可验证实现的严格基础。本文解决了这一差距，通过开发TMS 2-RA，一个宽松的操作TM规范。我们将TMS 2-RA与RC 11（修复的C11内存模型，不允许负载缓冲）集成，为TM库及其客户端提供正式的语义。我们开发了一个逻辑，TARO，用于验证客户端程序，使用TMS 2-RA同步。我们还展示了如何TMS 2-RA可以实现的C11库，TML-RA，使用放松和释放获取原子，但保证所需的TMS 2-RA的同步属性。我们基准测试TML-RA，并表明它优于其顺序一致的对应在STAMP基准。最后，我们使用基于仿真的验证技术来证明TML-RA的正确性。我们的整个发展是由伊莎贝尔/霍尔证明助理支持。
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.