Persistency semantics of the Intel-x86 architecture

File Description SizeFormat 
PersistencySemanticsOfTheIntelx86.pdfPublished version522.74 kBAdobe PDFView/Open
Title: Persistency semantics of the Intel-x86 architecture
Authors: Raad, A
Wickerson, J
Neiger, G
Vafeiadis, V
Item 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.
Issue Date: 1-Jan-2020
Date of Acceptance: 9-Oct-2019
DOI: 10.1145/3371079
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
Copyright Statement: © 2020 Copyright held by the owner/author(s). This work is licensed under a Creative Commons Attribution 4.0 International License ( ).
Sponsor/Funder: Engineering & Physical Science Research Council (E
Funder's Grant Number: Ref: 542716
Conference Name: ACM Principles of Programming Languages
Publication Status: Published
Start Date: 2020-01-19
Finish Date: 2020-01-25
Conference Place: Virtual
Open Access location:
Online Publication Date: 2019-12-20
Appears in Collections:Computing
Electrical and Electronic Engineering
Faculty of Engineering