Publications

BibTex format

@article{Raad:2020:10.1145/3428219,
author = {Raad, A and Lahav, O and Vafeiadis, V},
doi = {10.1145/3428219},
journal = {Proceedings of the ACM on Programming Languages},
pages = {1--28},
title = {Persistent owicki-gries reasoning: a program logic for reasoning about persistent programs on Intel-x86},
url = {http://dx.doi.org/10.1145/3428219},
volume = {4},
year = {2020}
}

Download

RIS format (EndNote, RefMan)

TY  - JOUR
AB  - The advent of non-volatile memory (NVM) technologies is expected to transform how software systems are structured fundamentally, making the task of correct programming significantly harder. This is because ensuring that memory stores persist in the correct order is challenging, and requires low-level programming to flush the cache at appropriate points. This has in turn resulted in a noticeable verification gap.To address this, we study the verification of NVM programs, and present Persistent Owicki-Gries (POG), the first program logic for reasoning about such programs. We prove the soundness of POG over the recent Intel-x86 model, which formalises the out-of-order persistence of memory stores and the semantics of the Intel cache line flush instructions. We then use POG to verify several programs that interact with NVM.
AU  - Raad,A
AU  - Lahav,O
AU  - Vafeiadis,V
DO  - 10.1145/3428219
EP  - 28
PY  - 2020///
SN  - 2475-1421
SP  - 1
TI  - Persistent owicki-gries reasoning: a program logic for reasoning about persistent programs on Intel-x86
T2  - Proceedings of the ACM on Programming Languages
UR  - http://dx.doi.org/10.1145/3428219
UR  - https://dl.acm.org/doi/10.1145/3428219
UR  - http://hdl.handle.net/10044/1/97398
VL  - 4
ER  -

Download

DrAzaleaRaad

Contact

Location

Summary

Citation

BibTex format

RIS format (EndNote, RefMan)