The semantics of transactions and weak memory in x86, power, ARM, and C++

File Description SizeFormat 
paper.pdfFile embargoed until 01 January 10000786.79 kBAdobe PDF    Request a copy
Title: The semantics of transactions and weak memory in x86, power, ARM, and C++
Authors: Chong, N
Sorensen, T
Wickerson, JP
Item 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.
Issue Date: 18-Jun-2018
Date of Acceptance: 12-Feb-2018
URI: http://hdl.handle.net/10044/1/58298
Publisher: Association for Computing Machinery (ACM)
Journal / Book Title: Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)
Copyright Statement: This paper is embargoed until publication.
Sponsor/Funder: Imperial College London
Engineering and Physical Sciences Research Council
Funder's Grant Number: Imperial College London
EP/K034448/1
Conference Name: ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)
Publication Status: Accepted
Start Date: 2018-06-18
Finish Date: 2018-06-22
Conference Place: Philadelphia, PA, USA
Embargo Date: publication subject to indefinite embargo
Appears in Collections:Faculty of Engineering
Electrical and Electronic Engineering



Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.

Creative Commons