Persistency semantics of the Intel-x86 architecture
File(s)
Published version
Author(s)
Raad, Azalea
Wickerson, John
Neiger, Gil
Vafeiadis, Viktor
Type
Conference Paper
Abstract
Emerging non-volatile memory (NVM) technologies promise the durability of disks with the performance of RAM. To describe the persistency guarantees of NVM, several memory persistency models have been proposed in the literature. However, the persistency semantics of the ubiquitous x86 architecture remains unexplored to date. To close this gap, we develop the Px86 (‘persistent x86’) model, formalising the persistency semantics of Intel-x86 for the first time. We formulate Px86 both operationally and declaratively, and prove that the two characterisations are equivalent. To demonstrate the application of Px86, we develop two persistent libraries over Px86: a persistent transactional library, and a persistent variant of the Michael–Scott queue. Finally, we encode our declarative Px86 model in Alloy and use it to generate persistency litmus tests automatically.
Date Issued
2020-01-01
Date Acceptance
2019-10-09
Citation
Proceedings of the ACM on Programming Languages (POPL2020), 2020, 4 (POPL), pp.11:1-11:31
ISSN
2475-1421
Publisher
Association for Computing Machinery (ACM)
Start Page
11:1
End Page
11:31
Journal / Book Title
Proceedings of the ACM on Programming Languages (POPL2020)
Volume
4
Issue
POPL
Replaces
10044/1/73858
Copyright Statement
© 2020 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
Engineering & Physical Science Research Council (E
Grant Number
Ref: 542716
Source
ACM Principles of Programming Languages
Publication Status
Published
Start Date
2020-01-19
Finish Date
2020-01-25
Coverage Spatial
Virtual
Date Publish Online
2019-12-20