View-Based Owicki-Gries Reasoning for Persistent x86-TSO (Extended Version)
Programming Languages
2022-01-19 v1 Logic in Computer Science
Abstract
The rise of persistent memory is disrupting computing to its core. Our work aims to help programmers navigate this brave new world by providing a program logic for reasoning about x86 code that uses low-level operations such as memory accesses and fences, as well as persistency primitives such as flushes. Our logic, Pierogi, benefits from a simple underlying operational semantics based on views, is able to handle optimised flush operations, and is mechanised in the Isabelle/HOL proof assistant. We detail the proof rules of Pierogi and prove them sound. We also show how Pierogi can be used to reason about a range of challenging single- and multi-threaded persistent programs.
Cite
@article{arxiv.2201.05860,
title = {View-Based Owicki-Gries Reasoning for Persistent x86-TSO (Extended Version)},
author = {Eleni Vafeiadi Bila and Brijesh Dongol and Ori Lahav and Azalea Raad and John Wickerson},
journal= {arXiv preprint arXiv:2201.05860},
year = {2022}
}
Comments
Extended version of the paper published in ESOP 2022