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{Cho:2021:10.1145/3453483.3454027,
author = {Cho, K and Lee, S-H and Raad, A and Kang, J},
doi = {10.1145/3453483.3454027},
pages = {16--31},
publisher = {ACM},
title = {Revamping hardware persistency models: view-based and axiomatic persistency models for Intel-x86 and Armv8},
url = {http://dx.doi.org/10.1145/3453483.3454027},
year = {2021}
}
Download

RIS format (EndNote, RefMan)

TY  - CPAPER
AB  - Non-volatile memory (NVM) is a cutting-edge storage technology that promises the performance of DRAM with the durability of SSD. Recent work has proposed several persistency models for mainstream architectures such as Intel-x86 and Armv8, describing the order in which writes are propagated to NVM. However, these models have several limitations; most notably, they either lack operational models or do not support persistent synchronization patterns.We close this gap by revamping the existing persistency models. First, inspired by the recent work on promising semantics, we propose a unified operational style for describing persistency using views, and develop view-based operational persistency models for Intel-x86 and Armv8, thus presenting the first operational model for Armv8 persistency. Next, we propose a unified axiomatic style for describing hardware persistency, allowing us to recast and repair the existing axiomatic models of Intel-x86 and Armv8 persistency. We prove that our axiomatic models are equivalent to the authoritative semantics reviewed by Intel and Arm engineers. We further prove that each axiomatic hardware persistency model is equivalent to its operational counterpart. Finally, we develop a persistent model checking algorithm and tool, and use it to verify several representative examples.
AU  - Cho,K
AU  - Lee,S-H
AU  - Raad,A
AU  - Kang,J
DO  - 10.1145/3453483.3454027
EP  - 31
PB  - ACM
PY  - 2021///
SP  - 16
TI  - Revamping hardware persistency models: view-based and axiomatic persistency models for Intel-x86 and Armv8
UR  - http://dx.doi.org/10.1145/3453483.3454027
UR  - https://dl.acm.org/doi/10.1145/3453483.3454027
ER  -
Download