Nathan Chong, ARM; Tyler Sorensen and John Wickerson, Imperial College London
Best Paper at PLDI 2018: Link to Paper (external site)
Weak memory models provide a complex, system-centric semantics for concurrent programs, while transactional memory (TM) provides a simpler, programmer-centric semantics. Both have been studied in detail, but their combined semantics is not well understood. This is problematic because such widely-used architectures and languages as x86, Power, and C++ all support TM, and all have weak memory models.
Our work aims to clarify the interplay between weak memory and TM by extending existing axiomatic weak memory models (x86, Power, ARMv8, and C++) with new rules for TM. Our formal models are backed by automated tooling that enables (1) the synthesis of tests for validating our models against existing implementations and (2) the model-checking of TM-related transformations, such as lock elision and compiling C++ transactions to hardware. A key finding is that a proposed TM extension to ARMv8 currently being considered within ARM Research is incompatible with lock elision without sacrificing portability or performance.
Open Access Media
USENIX is committed to Open Access to the research presented at our events. Papers and proceedings are freely available to everyone once the event begins. Any video, audio, and/or slides that are posted after the event are also free and open to everyone. Support USENIX and our commitment to Open Access.
title = {The Semantics of Transactions and Weak Memory in x86, Power, {ARM}, and C++},
booktitle = {2019 USENIX Annual Technical Conference (USENIX ATC 19)},
year = {2019},
address = {Renton, WA},
url = {https://www.usenix.org/conference/atc19/presentation/chong},
publisher = {USENIX Association},
month = jul
}