Paper Info
Title
The Semantics of Transactions and Weak Memory in x86, Power, ARM, and C++.
Abstract
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.
Year
DOI
Venue
2017
10.1145/3192366.3192373
PLDI '18: ACM SIGPLAN Conference on Programming Language Design and Implementation Philadelphia PA USA June, 2018
Keywords
Field
DocType
Program Synthesis, Shared Memory Concurrency, Transactional Memory, Weak Memory
x86,Computer science,Parallel computing,Semantics
Journal
Volume
Issue
ISSN
abs/1710.04839
4
Proceedings of 39th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'18), ACM, New York, NY, USA. 2018
ISBN
Citations 
PageRank 
978-1-4503-5698-5
3
0.38
References 
Authors
31
3
Name
Order
Citations
PageRank
Nathan Chong11857.91
Tyler Sorensen21099.42
John Wickerson3357.17