24
IRUS Total
Downloads
  Altmetric

Persistence semantics for weak memory: integrating epoch persistency with the TSO memory model.

File Description SizeFormat 
PTSO.pdfPublished version453.84 kBAdobe PDFView/Open
Title: Persistence semantics for weak memory: integrating epoch persistency with the TSO memory model.
Authors: Raad, A
Vafeiadis, V
Item Type: Journal Article
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 semantics of such persistency models in the context of existing mainstream hardware has been unexplored to date. To close this gap, we integrate the buffered epoch persistency model with the 'total-store-order' (TSO) memory model of the x86 and SPARC architectures. We thus develop the PTSO ('persistent' TSO) model and formalise its semantics both operationally and declaratively. We demonstrate that the two characterisations of PTSO are equivalent. We then formulate the notion of persistent linearisability to establish the correctness of library implementations in the context of persistent memory. To showcase our formalism, we develop two persistent implementations of a queue library, and apply persistent linearisability to show their correctness.
Issue Date: 1-Nov-2018
Date of Acceptance: 1-Nov-2018
URI: http://hdl.handle.net/10044/1/75941
DOI: 10.1145/3276507
ISSN: 2475-1421
Publisher: Association for Computing Machinery (ACM)
Start Page: 137:1
End Page: 137:27
Journal / Book Title: Proceedings of the ACM on Programming Languages
Volume: 2
Copyright Statement: © 2018 Copyright held by the owner/author(s). This work is licensed under a Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/)
Publication Status: Published
Open Access location: https://dl.acm.org/doi/pdf/10.1145/3276507?download=true
Article Number: Article No.: 137
Online Publication Date: 2018-11-01
Appears in Collections:Computing