The semantics of transactions and weak memory in x86, power, ARM, and C++
File(s)paper.pdf (786.79 KB)
Accepted version
Author(s)
Chong, Nathan
Sorensen, Tyler
Wickerson, JP
Type
Conference Paper
Abstract
Weak memory models provide a complex, system-centric se-
mantics for concurrent programs, while transactional mem-
ory (TM) provides a simpler, programmer-centric semantics.
Both have been studied in detail, but their
combined
seman-
tics 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 mem-
ory 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 com-
piling C++ transactions to hardware. A key finding is that a
proposed TM extension to ARMv8 currently being consid-
ered within ARM Research is incompatible with lock elision
without sacrificing portability or performance.
mantics for concurrent programs, while transactional mem-
ory (TM) provides a simpler, programmer-centric semantics.
Both have been studied in detail, but their
combined
seman-
tics 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 mem-
ory 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 com-
piling C++ transactions to hardware. A key finding is that a
proposed TM extension to ARMv8 currently being consid-
ered within ARM Research is incompatible with lock elision
without sacrificing portability or performance.
Date Acceptance
2018-02-12
Citation
Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)
Publisher
Association for Computing Machinery (ACM)
Journal / Book Title
Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)
Copyright Statement
© 2018 IEEE. Personal use of this material is permitted. Permission from IEEE must be obtained for all other uses, in any current or future media, including reprinting/republishing this material for advertising or promotional purposes, creating new collective works, for resale or redistribution to servers or lists, or reuse of any copyrighted component of this work in other works.
Sponsor
Imperial College London
Engineering and Physical Sciences Research Council
Grant Number
Imperial College London
EP/K034448/1
Source
ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)
Subjects
Software Engineering
Publication Status
Accepted
Start Date
2018-06-18
Finish Date
2018-06-22
Coverage Spatial
Philadelphia, PA, USA