Persistence semantics for weak memory: integrating epoch persistency with the TSO memory model.
File(s)PTSO.pdf (453.84 KB)
Published version
Author(s)
Raad, Azalea
Vafeiadis, Viktor
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.
Date Issued
2018-11-01
Date Acceptance
2018-11-01
Citation
Proceedings of the ACM on Programming Languages, 2018, 2, pp.137:1-137:27
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/)
This work is licensed under a Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/)
Identifier
https://dl.acm.org/doi/10.1145/3276507
Source
ACM Object-Oriented Programming, Systems, Languages & Applications (OOPSLA18)
Publication Status
Published
Article Number
Article No.: 137
Date Publish Online
2018-11-01