Implementing and Verifying Release-Acquire Transactional Memory (Extended Version)
Sadegh Dalvandi, Brijesh Dongol

TL;DR
This paper develops a formal specification and verification framework for relaxed transactional memory under C11, introduces a new implementation, and demonstrates its efficiency and correctness through benchmarks and formal proofs.
Contribution
It presents TMS2-RA, a formal relaxed TM specification integrated with C11, and provides a verified, efficient implementation using Isabelle/HOL.
Findings
TML-RA outperforms sequentially consistent implementations in benchmarks.
The formal semantics enable rigorous verification of relaxed TM implementations.
The approach combines formal methods with practical benchmarking for TM correctness and performance.
Abstract
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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsDistributed systems and fault tolerance · Cognitive Functions and Memory · Mobile Agent-Based Network Management
