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 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.