Imperial College London
Portrait Picture

DrAzaleaRaad

Faculty of Engineering, Department of Computing

Senior Lecturer
 
 
 
//

Contact

 

+44 (0)20 7594 8271azalea.raad Website

 
 
//

Location

 

426Huxley BuildingSouth Kensington Campus

//

Summary

 

Publications

Citation

BibTex format

@inproceedings{Raad:2018:10.1145/3276507,
author = {Raad, A and Vafeiadis, V},
doi = {10.1145/3276507},
pages = {137:1--137:27},
publisher = {Association for Computing Machinery (ACM)},
title = {Persistence semantics for weak memory: integrating epoch persistency with the TSO memory model.},
url = {http://dx.doi.org/10.1145/3276507},
year = {2018}
}
Download

RIS format (EndNote, RefMan)

TY  - CPAPER
AB  - 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.
AU  - Raad,A
AU  - Vafeiadis,V
DO  - 10.1145/3276507
EP  - 1
PB  - Association for Computing Machinery (ACM)
PY  - 2018///
SN  - 2475-1421
SP  - 137
TI  - Persistence semantics for weak memory: integrating epoch persistency with the TSO memory model.
UR  - http://dx.doi.org/10.1145/3276507
UR  - https://dl.acm.org/doi/10.1145/3276507
UR  - http://hdl.handle.net/10044/1/75941
ER  -
Download