Implementing and Verifying Release-Acquire Transactional Memory in C11
summary
Defines a relaxed transactional-memory spec called TMS2-ra integrated with RC11 (view-based RC11) and a program logic TARO, implements the spec as a C11 library TML-ra that uses relaxed and release‑acquire atomics, and proves contextual refinement of TML-ra to TMS2-ra by a simulation proof formalized in Isabelle/HOL. Benchmarks on STAMP show TML-ra often outperforms the sequentially consistent variant; the implementation and proofs are mechanized and validated.
AI-written summary · about
chapters (21)
- 0:00Release-acquire transactional memory
- 1:26Fixing message passing with atomics
- 3:13Limitations of relaxed CAS
- 5:39Extending to transactions
- 7:26Wrapping operations in transactions
- 8:28Chaining transactions
- 9:33Operational semantics for RC11
- 10:58Opacity and consistency in TMS2
- 13:27Execution example
- 14:52Transactions with release-acquire
- 15:54Relaxed transactions and snapshots
- 16:37Specification overview
- 17:44Implementing transactional mutex
- 18:28Benchmarking release-acquire vs SC
- 19:10Proof of correctness
- 21:38Transactional weak memory
- 24:07Owicki-Gries proof
- 25:11Summary and future work
- 26:20Q&A: Axiomatic vs operational
- 27:44Q&A: Instruction reordering
- 29:48Q&A
related talks
01h 00mWhat did C++ do for Transactional Memory?
23mAn Operational Approach to Library Abstraction under Relaxed Memory Concurrency
01h 13mTransactional memory
19mVerifying General-Purpose RCU for Reclamation in Relaxed Memory Separation Logic
01h 33mWhy You Should Use Software Transactional Memory
15mOptimal Reads-From Consistency Checking for C11-Style Memory Models
01h 03m“Transactional Memory in Practice"
23mMemory Consistency Model Status Update