Implementing and Verifying Release-Acquire Transactional Memory in C11
Implementing and Verifying Release-Acquire Transactional Memory in C11
复制标题
DOI：
10.1145/3563352
复制
发表时间：
2022-10-01
影响因子：
1.8
通讯作者：
Dongol，Brijesh
中科院分区：
文献类型：
--
作者：
Dalvandi，Sadegh;Dongol，Brijesh
事务性内存（TM）是一种被深入研究的同步范式，在软件和硬件及其组合中有许多被提议的实现。然而，放松记忆下的TM，例如C11（2011年C/ c++标准）仍然知之甚少，缺乏支持可验证实现的严格基础。本文通过开发TMS2-ra（一种宽松的可操作TM规范）来解决这一差距。我们将TMS2-ra与RC11（修复后的不允许负载缓冲的C11内存模型）集成在一起，为TM库及其客户端提供形式化语义。我们开发了一个逻辑TARO，用于验证使用TMS2-ra进行同步的客户端程序。我们还展示了如何通过C11库TML-ra实现TMS2-ra，该库使用放松原子和释放获取原子，同时保证TMS2-ra所需的同步属性。我们对TML-ra进行了基准测试，并表明它优于STAMP基准测试中顺序一致的对应项。最后，我们使用基于仿真的验证技术来证明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.