Publications

BibTex format

@inproceedings{Bila:2022:10.1007/978-3-030-99336-8_9,
author = {Bila, E and Dongol, B and Lahav, O and Raad, A and Wickerson, J},
doi = {10.1007/978-3-030-99336-8_9},
pages = {234--261},
publisher = {Springer},
title = {View-based Owicki-Gries reasoning for persistent x86-TSO},
url = {http://dx.doi.org/10.1007/978-3-030-99336-8_9},
year = {2022}
}

Download

RIS format (EndNote, RefMan)

TY  - CPAPER
AB  - The rise of persistent memory is disrupting computing toits core. Our work aims to help programmers navigate this brave newworld by providing a program logic for reasoning about x86 code thatuses low-level operations such as memory accesses and fences, as well aspersistency primitives such as flushes. Our logic, Pierogi, benefits from asimple underlying operational semantics based on views, is able to handleoptimised flush operations, and is mechanised in the Isabelle/HOL proofassistant. We detail the proof rules of Pierogi and prove them sound.We also show how Pierogi can be used to reason about a range ofchallenging single- and multi-threaded persistent programs
AU  - Bila,E
AU  - Dongol,B
AU  - Lahav,O
AU  - Raad,A
AU  - Wickerson,J
DO  - 10.1007/978-3-030-99336-8_9
EP  - 261
PB  - Springer
PY  - 2022///
SN  - 0302-9743
SP  - 234
TI  - View-based Owicki-Gries reasoning for persistent x86-TSO
UR  - http://dx.doi.org/10.1007/978-3-030-99336-8_9
UR  - http://link.springer.com/chapter/10.1007/978-3-030-99336-8_9
UR  - http://hdl.handle.net/10044/1/95468
ER  -

Download

DrAzaleaRaad

Contact

Location

Summary

Citation

BibTex format

RIS format (EndNote, RefMan)