IRUS Total

Weak persistency semantics from the ground up: formalising the persistency semantics of ARMv8 and transactional models

File Description SizeFormat 
oopsla19main-p83-p.pdfpublished version905.08 kBAdobe PDFView/Open
Title: Weak persistency semantics from the ground up: formalising the persistency semantics of ARMv8 and transactional models
Authors: Raad, A
Wickerson, J
Vafeiadis, V
Item Type: Conference Paper
Abstract: Emerging non-volatile memory (NVM) technologies promise the durability of disks with the performance of volatile memory (RAM). To describe the persistency guarantees of NVM, several memory persistency models have been proposed in the literature. However, the formal persistency semantics of mainstream hardware is unexplored to date. To close this gap, we present a formal declarative framework for describing concurrency models in the NVM context, and then develop the PARMv8 persistency model as an instance of our framework, formalising the persistency semantics of the ARMv8 architecture for the first time. To facilitate correct persistent programming, we study transactions as a simple abstraction for concurrency and persistency control. We thus develop the PSER (persistent serialisability) persistency model, formalising transactional semantics in the NVM context for the first time, and demonstrate that PSER correctly compiles to PARMv8. This then enables programmers to write correct, concurrent and persistent programs, without having to understand the low-level architecture-specific persistency semantics of the underlying hardware.
Issue Date: 10-Oct-2019
Date of Acceptance: 31-Aug-2019
URI: http://hdl.handle.net/10044/1/74999
DOI: 10.1145/3360561
ISSN: 2475-1421
Publisher: Association for Computing Machinery (ACM)
Journal / Book Title: Proceedings of the ACM on Programming Languages
Volume: 3
Copyright Statement: ©2019 Copyright held by the owner/author(s). This work is licensed under a Creative Commons Attribution 4.0 International License (https://creativecommons.org/licenses/by/4.0/)
Sponsor/Funder: Engineering & Physical Science Research Council (E
Funder's Grant Number: 542716
Conference Name: OOPSLA 2019
Publication Status: Published
Start Date: 2019-10-20
Finish Date: 2019-10-25
Conference Place: Athens, Greece
Appears in Collections:Electrical and Electronic Engineering
Faculty of Engineering